Skip to content
Snippets Groups Projects
Commit 53cd110f authored by Tim van Dijen's avatar Tim van Dijen
Browse files

Fix: build docs on push

parent 8205f8e0
No related branches found
No related tags found
No related merge requests found
......@@ -37,8 +37,8 @@ jobs:
runs-on: [ubuntu-latest]
steps:
- name: Run docs build if any of markdown-files have changed
if: steps.changed-files-specific.outputs.any_changed == 'true' && github.event_name != 'pull_request'
- name: Run docs build
if: github.event_name != 'pull_request'
uses: actions/github-script@v6
with:
# Token has to be generated on a user account that controls the docs-repository.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment