Jonathan provides new P/R for 3003 #587
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 | |
| # and then regenerating the meta-data/dates file from scratch (slow!) | |
| 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: Generate HTML lists | |
| run: make lists | |
| # We need a fresh repo that has valid credentials to push to gh-pages. | |
| - 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 ; 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 .. |