diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-05-03 22:15:36 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-03 13:15:36 -0700 |
| commit | 439ab123cccdbf4f046b4e084ce996a1dc2aa758 (patch) | |
| tree | 3ebca4f480385c603518a214fac4064e0c62dc83 /.github/workflows | |
| parent | 009ae6e41ace0a80923e02941a0bbc80de6e84f1 (diff) | |
Add missing --auto-download in CI (#6478)
This PR adds --auto-download for the CI job that builds the documentation. Also makes sure that the documentation workflow never fails.
Diffstat (limited to '.github/workflows')
| -rw-r--r-- | .github/workflows/docs_update.yml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/.github/workflows/docs_update.yml b/.github/workflows/docs_update.yml index c51246ee0..9c733728f 100644 --- a/.github/workflows/docs_update.yml +++ b/.github/workflows/docs_update.yml @@ -31,6 +31,7 @@ on: jobs: build: runs-on: ubuntu-latest + continue-on-error: true steps: - uses: actions/checkout@v2 @@ -63,7 +64,8 @@ jobs: echo "Identified PR #$NAME (from $PRHASH)" NAME="pr$NAME" # be careful here, see explanation above! - git fetch + git remote add pr "${{ github.event.pull_request.head.repo.clone_url}}" + git fetch pr "${{ github.event.pull_request.head.ref}}:pr" git checkout "${PRHASH}" -- \ `git ls-tree "${PRHASH}" --name-only -r docs/ | grep -E ".*\.(rst|bib)"` \ `git ls-tree "${PRHASH}" --name-only -r src/api/ | grep -E ".*\.(h|cpp|java|py)"` \ @@ -72,7 +74,7 @@ jobs: echo "NAME=$NAME" >> $GITHUB_ENV - name: Configure - run: ./configure.sh production --docs --all-bindings + run: ./configure.sh production --docs --all-bindings --auto-download - name: Build run: make -j2 docs-gh |