Skip to content

Commit 1415bff

Browse files
committed
Update comments in deploy.yml
The caching is no longer for meta-data/dates thanks to Tim's make_dates.py, but is still faster than cloning the full history every time.
1 parent 0eebfbd commit 1415bff

File tree

1 file changed

+9
-4
lines changed

1 file changed

+9
-4
lines changed

.github/workflows/deploy.yml

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,8 @@ jobs:
1313

1414
steps:
1515
- name: Use cached git repo
16-
# Try to use a cached copy of the repository to avoid cloning it again
17-
# and then regenerating the meta-data/dates file from scratch (slow!)
16+
# Try to use a cached copy of the repository to avoid cloning it again,
17+
# as cloning the full history (needed for timestamps) takes two minutes.
1818
id: cache-repo
1919
uses: actions/cache@v4
2020
with:
@@ -50,10 +50,15 @@ jobs:
5050
- name: Update issue timestamps
5151
run: make dates
5252

53+
- name: Build programs
54+
run: make pgms -j 4
55+
5356
- name: Generate HTML lists
5457
run: make lists
5558

56-
# We need a fresh repo that has valid credentials to push to gh-pages.
59+
# The cached repo might have a stale API token that can't push changes.
60+
# Clone a fresh repo that has valid credentials to push to gh-pages.
61+
# The default fetch-depth:1 is OK for this step.
5762
- name: Clone repo again in order to push
5863
uses: actions/checkout@v4
5964
with:
@@ -74,7 +79,7 @@ jobs:
7479
# This only compares the staged changes, so ignores new timestamps
7580
# in the lwg-*.html files. The commit -a will pick those up though.
7681
printf '\nChecking HTML issues for changes ...\n'
77-
if git diff --cached --exit-code ; then
82+
if git diff --cached --exit-code --name-status ; then
7883
echo 'No changes, not publishing new lists.'
7984
else
8085
printf '\nCommitting the changes above:\n'

0 commit comments

Comments
 (0)