1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
name: Bootstrap Skip
# This Workflow is special and contains a workaround for a known limitation of GitHub CI.
#
# The problem: We don't want to run the "bootstrap" jobs on PRs which contain only changes
# to the docs, since these jobs take a long time to complete without providing any benefit.
# We therefore use path-filtering in the workflow triggers for the bootstrap jobs, namely
# "paths-ignore: doc/**". But the "Bootstrap post job" is a required job, therefore a PR cannot
# be merged unless the "Bootstrap post job" completes succesfully, which it doesn't do if we
# filter it out.
#
# The solution: We use a second job with the same name which always returns the exit code 0.
# The logic implemented for "required" workflows accepts if 1) at least one job with that name
# runs through, AND 2) If multiple jobs of that name exist, then all jobs of that name have to
# finish successfully.
on:
push:
paths:
- 'doc/**'
- '**/README.md'
- 'CONTRIBUTING.md'
branches:
- master
pull_request:
paths:
- 'doc/**'
- '**/README.md'
- 'CONTRIBUTING.md'
release:
types:
- created
jobs:
bootstrap-post-job:
if: always()
name: Bootstrap post job
runs-on: ubuntu-latest
steps:
- run: exit 0
|
