File tree Expand file tree Collapse file tree 1 file changed +5
-7
lines changed
Expand file tree Collapse file tree 1 file changed +5
-7
lines changed Original file line number Diff line number Diff line change 1- name : Build manual
1+ name : Docs
22
3- # Trigger the workflow on push or pull request or manually
3+ # Trigger the workflow on push or pull request
44on :
5- workflow_dispatch :
65 push :
76 branches :
7+ - main
88 - master
99 pull_request :
1010
1111# the `concurrency` settings ensure that not too many CI jobs run in parallel
1212concurrency :
1313 # group by workflow and ref; the last slightly strange component ensures that for pull
14- # requests, we limit to 1 concurrent job, but for the master branch we don't
15- group : ${{ github.workflow }}-${{ github.ref }}-${{ github.ref != 'refs/heads/master' || github.run_number }}
14+ # requests, we limit to 1 concurrent job, but for the default repository branch we don't
15+ group : ${{ github.workflow }}-${{ github.ref }}-${{ github.ref_name != github.event.repository.default_branch || github.run_number }}
1616 # Cancel intermediate builds, but only if it is a pull request build.
1717 cancel-in-progress : ${{ startsWith(github.ref, 'refs/pull/') }}
1818
1919jobs :
20- # The documentation job
2120 manual :
2221 name : Build manuals
2322 runs-on : ubuntu-latest
3130 - name : ' Upload documentation'
3231 uses : actions/upload-artifact@v4
3332 with :
34- retention-days : 7
3533 name : manual
3634 path : ./doc/manual.pdf
3735 if-no-files-found : error
You can’t perform that action at this time.
0 commit comments