File tree Expand file tree Collapse file tree 2 files changed +13
-13
lines changed
Expand file tree Collapse file tree 2 files changed +13
-13
lines changed Original file line number Diff line number Diff line change 1010# the `concurrency` settings ensure that not too many CI jobs run in parallel
1111concurrency :
1212 # group by workflow and ref; the last slightly strange component ensures that for pull
13- # requests, we limit to 1 concurrent job, but for the master branch we don't
14- group : ${{ github.workflow }}-${{ github.ref }}-${{ github.ref != 'refs/heads/master' || github.run_number }}
13+ # requests, we limit to 1 concurrent job, but for the default repository branch we don't
14+ group : ${{ github.workflow }}-${{ github.ref }}-${{ github.ref_name != github.event.repository.default_branch || github.run_number }}
1515 # Cancel intermediate builds, but only if it is a pull request build.
1616 cancel-in-progress : ${{ startsWith(github.ref, 'refs/pull/') }}
1717
@@ -25,12 +25,12 @@ jobs:
2525 matrix :
2626 gap-branch :
2727 - master
28+ - stable-4.15
2829 - stable-4.14
2930 - stable-4.13
3031 - stable-4.12
3132 - stable-4.11
3233 - stable-4.10
33- - stable-4.9
3434
3535 steps :
3636 - uses : actions/checkout@v5
Original file line number Diff line number Diff line change 22set -e
33
44echo " TeXing documentation"
5+ # delete old stuff to avoid spurious or "hidden errors" caused by their presence
6+ rm -f manual.aux manual.pdf manual.idx manual.ilg manual.ind manual.lab manual.log manual.six manual.toc
7+
58# TeX the manual
69tex manual
7- # ... and build its bibliography (uncomment if there is a `manual.bib')
10+ # ... and build its bibliography
811bibtex manual
9- # TeX the manual again to incorporate the ToC ... and build the index
10- tex manual
12+ # TeX the manual again to incorporate the ToC
1113tex manual
14+ # ... and build the index
1215../../../doc/manualindex manual
1316# Finally TeX the manual again to get cross-references right
1417tex manual
18+
1519# Create PDF version
16- pdftex manual; pdftex manual
20+ pdftex manual
21+ pdftex manual
1722
1823# The HTML version of the manual
19- rm -rf ../htm
20- mkdir ../htm
24+ mkdir -p ../htm
2125echo " Creating HTML documentation"
2226../../../etc/convert.pl -i -u -c -n ModIsom . ../htm
23-
24- # ############################################################################
25- # #
26- # E
You can’t perform that action at this time.
0 commit comments