Fix incorrect comment in discussion of 4123 #675
This file contains 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
| # A workflow to update the online issues lists. | |
| name: Generate HTML pages | |
| on: | |
| # This job must only be run when changes are pushed to the master branch! | |
| push: | |
| branches: [ master ] | |
| jobs: | |
| update-html-pages: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Use cached git repo | |
| # Try to use a cached copy of the repository to avoid cloning it again, | |
| # as cloning the full history (needed for timestamps) takes two minutes. | |
| id: cache-repo | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| .git | |
| xml | |
| meta-data | |
| src | |
| key: cached-repo | |
| - if: ${{ steps.cache-repo.outputs.cache-hit == 'true' }} | |
| # Using cached git repo, so sync with the latest changes. | |
| name: Update cached repo | |
| run: | | |
| # Make sure we are in a clean worktree on the right branch. | |
| git reset --hard HEAD | |
| git checkout master | |
| # Fetch changes since the cache was saved. | |
| git fetch | |
| # Update timestamp of this file so only issue files that get | |
| # changed by the next command will be newer than it. | |
| touch meta-data/dates | |
| # Do a hard reset instead of merge, just in case there has been | |
| # a force push since the cache was last updated. | |
| git reset --hard @{u} | |
| - if: ${{ steps.cache-repo.outputs.cache-hit != 'true' }} | |
| # Not using cached git repo, so clone it (with full history). | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: Update issue timestamps | |
| run: make dates | |
| - name: Build programs | |
| run: make pgms -j 4 | |
| - name: Generate HTML lists | |
| run: make lists | |
| # The cached repo might have a stale API token that can't push changes. | |
| # Clone a fresh repo that has valid credentials to push to gh-pages. | |
| # The default fetch-depth:1 is OK for this step. | |
| - name: Clone repo again in order to push | |
| uses: actions/checkout@v4 | |
| with: | |
| ref: 'gh-pages' | |
| path: 'gh-pages' | |
| clean: 'false' | |
| - name: Update online pages | |
| run: | | |
| : Push new HTML files to gh-pages branch | |
| mv mailing/*.html gh-pages/ | |
| rmdir mailing | |
| cd gh-pages | |
| git config user.name "github-actions" | |
| git config user.email "[email protected]" | |
| # Stage any changes to the individual issues (including new files): | |
| git add issue*.html | |
| # This only compares the staged changes, so ignores new timestamps | |
| # in the lwg-*.html files. The commit -a will pick those up though. | |
| printf '\nChecking HTML issues for changes ...\n' | |
| if git diff --cached --exit-code --name-status ; then | |
| echo 'No changes, not publishing new lists.' | |
| else | |
| printf '\nCommitting the changes above:\n' | |
| git commit -a -m 'Automatic update from GitHub Actions workflow' | |
| printf '\nPushing to the gh-pages branch:\n' | |
| git push | |
| fi | |
| cd .. |