chore: ensured unified .gitattributes (#792) #24
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
| # Shallow clone default branch and merge the PR using only plain git | |
| # | |
| # 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 squashed | |
| # merges of pull requests, immediately after a workflow re-run. | |
| # | |
| # To be pedantic clear, Github's pull requests calculate the merge | |
| # points of PRs, but only at the PR's "synchronize" event. This | |
| # does *not* include changes on master/main, *or* 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. Re-running workflows also | |
| # changes nothing. | |
| # | |
| # Notes: | |
| # - clone --depth=1 downloads the same data as actions/checkout; | |
| # - clone --filter=tree:0 implies --depth=1, and also download the | |
| # linear commit history of the branch; | |
| # - github.event.pull_request.head.sha maps to the PR tip, not merged. | |
| # | |
| # Does not work: | |
| # - clone --depth=1 and merge from PR SHA, with or without fetch by SHA; | |
| # - clone --single-branch and merge from PR SHA, without fetch by SHA. | |
| name: Build and validate XML | |
| on: | |
| push: | |
| pull_request: | |
| jobs: | |
| build: | |
| name: Run configure | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Clone repositories | |
| run: | | |
| # Shallow clones | |
| set -x | |
| git clone -q --depth=1 https://github.com/php/doc-base.git doc-base | |
| git clone -q --depth=1 https://github.com/php/doc-en.git en | |
| git clone -q --filter=tree:0 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}" | |
| set -x | |
| git fetch -q --filter=tree:0 origin ${{ github.event.pull_request.head.sha }} | |
| git merge -q -m "$message" ${{ 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 |