Make CI checks to always merge into current main/master #9
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Build XML | |
| on: | |
| push: | |
| branches: | |
| - master | |
| pull_request: | |
| branches: | |
| - master | |
| jobs: | |
| build: | |
| name: Run configure | |
| runs-on: ubuntu-latest | |
| steps: | |
| # Shallow clone default branches and merge PR using only plain git: | |
| # | |
| # - clone --single-branch selects the default branch; | |
| # - clone --depth=1 downloads the same data as actions/checkout; | |
| # - github.event.pull_request.head.sha maps to the not merged PR tip. | |
| # | |
| # Avoids getting stuck in the past, like GH actions/checkout does, and | |
| # we do not need any other stuff for building the manual. The results | |
| # of workflow re-runs always match with results of normal or squash | |
| # merging the pull requests, immediately after a workflow re-run. | |
| # | |
| # To be pedantic clear, Github's pull requests only merge the PRs on the | |
| # "synchronize" event. That does *not* include workflows re-runs. So in | |
| # busy repositories, the results of CI checks are almost always outdated | |
| # and invalid, not representing the future state of the default branch | |
| # after the pull request is merged, even after workflows re-runs. | |
| # | |
| # In theory, --filter=blob:none on clone of to be merged repository | |
| # would be faster, and avoid an extra git fetch on PR tip. But cause | |
| # subsequent piecewise downloads of blob data, both on default and | |
| # feature branches, that is slow. | |
| - name: Set up files | |
| run: | | |
| # Checkout repositories | |
| set -x | |
| git clone -q --depth=1 --single-branch https://github.com/php/doc-base.git doc-base | |
| git clone -q --depth=1 --single-branch https://github.com/php/doc-en.git en | |
| git clone -q --single-branch https://github.com/php/doc-pt_br.git pt_br | |
| - name: Merge pull request | |
| run: | | |
| # Plain git merge | |
| cd pt_br | |
| git config user.name "$GITHUB_ACTOR" | |
| git config user.email "$GITHUB_ACTOR@users.noreply.github.com" | |
| mainsha=$(git rev-parse HEAD) | |
| message="Merge ${{ github.event.pull_request.head.sha }} into ${mainsha}" | |
| echo $message | |
| set -x | |
| git fetch -q --no-tags --prune --no-recurse-submodules origin ${{ github.event.pull_request.head.sha }} | |
| git merge -q --no-edit ${{ github.event.pull_request.head.sha }} | |
| - name: Build manual.xml | |
| run: | | |
| php doc-base/configure.php --disable-libxml-check --enable-xml-details --redirect-stderr-to-stdout --with-lang=pt_br 2>&1 | |
| echo | |
| sha1sum doc-base/temp/manual.xml |