Skip to content

Finish improvements to the CI configuration for documentation changes #38

Finish improvements to the CI configuration for documentation changes

Finish improvements to the CI configuration for documentation changes #38

Workflow file for this run

name: Validate 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 "validate" 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 validate jobs, namely
# "paths-ignore: doc/**". But the "Validate post job" is a required job, therefore a PR cannot
# be merged unless the "Validate 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:
validate-post-job:
if: always()
name: Validate post job
runs-on: ubuntu-latest
steps:
- run: exit 0