Skip to content

Commit ec5b393

Browse files
committed
update-manual-pages: optionally force a complete rebuild
Sometimes a bug is found in the way the manual pages are built, requiring a change e.g. in the `update-docs.rb` script or in the corresponding style sheets. In such a case, the manual pages have to be rebuilt from scratch, even if they exist already. This commit introduces the `force-rebuild` flag to do this. Signed-off-by: Johannes Schindelin <[email protected]>
1 parent 9d9fe75 commit ec5b393

File tree

1 file changed

+26
-8
lines changed

1 file changed

+26
-8
lines changed

.github/workflows/update-git-version-and-manual-pages.yml

Lines changed: 26 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,11 @@ name: Synchronize with new Git version (if any)
22

33
on:
44
workflow_dispatch:
5+
inputs:
6+
force-rebuild:
7+
description: Force re-building all manual pages (e.g. after a script change)
8+
type: boolean
9+
default: false
510
schedule:
611
# check daily for updates
712
- cron: '37 17 * * *'
@@ -53,23 +58,36 @@ jobs:
5358
-m 'Updated via the `update-git-version-and-manual-pages.yml` GitHub workflow.' \
5459
-- hugo.yml
5560
- name: prepare worktree
56-
if: steps.commit.outputs.result != ''
61+
if: steps.commit.outputs.result != '' || inputs.force-rebuild == true
5762
run: git sparse-checkout disable
5863
- name: clone git.git
59-
if: steps.commit.outputs.result != ''
64+
if: steps.commit.outputs.result != '' || inputs.force-rebuild == true
6065
run: git clone --bare https://github.com/git/git '${{ runner.temp }}/git'
6166
- name: update manual pages
62-
if: steps.commit.outputs.result != ''
63-
run: bundle exec ruby script/update-docs.rb '${{ runner.temp }}/git' en
67+
if: steps.commit.outputs.result != '' || inputs.force-rebuild == true
68+
run: |
69+
if test true = '${{ inputs.force-rebuild }}'
70+
then
71+
export RERUN=true
72+
fi
73+
bundle exec ruby script/update-docs.rb '${{ runner.temp }}/git' en
6474
- name: commit manual pages
65-
if: steps.commit.outputs.result != ''
75+
id: manual-pages
76+
if: steps.commit.outputs.result != '' || inputs.force-rebuild == true
6677
run: |
6778
git add -A external/docs &&
79+
if test true = '${{ inputs.force-rebuild }}' && git diff-index --cached --quiet HEAD --
80+
then
81+
echo '::notice::A manual pages rebuild was requested but resulted in no changes' >&2
82+
exit 0
83+
fi &&
84+
version='${{ steps.commit.outputs.result }}' &&
6885
git \
6986
-c user.name=${{ github.actor }} \
7087
-c user.email=${{ github.actor }}@noreply.github.com \
71-
commit -m "Update manual pages (${{ steps.commit.outputs.result }})" \
72-
-m 'Updated via the `update-git-version-and-manual-pages.yml` GitHub workflow.'
88+
commit -m "Update manual pages (${version:-manually forced rebuild})" \
89+
-m 'Updated via the `update-git-version-and-manual-pages.yml` GitHub workflow.' &&
90+
echo "result=modified" >>$GITHUB_OUTPUT
7391
- name: verify that there are no uncommitted changes
7492
run: |
7593
git update-index --refresh &&
@@ -80,6 +98,6 @@ jobs:
8098
exit 1
8199
fi
82100
- name: deploy to GitHub Pages
83-
if: steps.commit.outputs.result != ''
101+
if: steps.commit.outputs.result != '' || steps.manual-pages.outputs.result != ''
84102
id: deploy
85103
uses: ./.github/actions/deploy-to-github-pages

0 commit comments

Comments
 (0)