Skip to content

Commit

Permalink
Merge pull request #1633 from GaloisInc/no_fork_deploy_docs
Browse files Browse the repository at this point in the history
Disable CI-based github page deployment for forks.
  • Loading branch information
kquick authored Feb 23, 2024
2 parents facc682 + 9e7f6f1 commit 5bbc3dc
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions .github/workflows/docs.yml
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,8 @@ jobs:
-p 'python3.withPackages (pp: [pp.sphinx pp.sphinx_rtd_theme])' \
--run 'make html'
build-pages-docs:
# Do not run this on forks:
if: github.event.pull_request.head.repo.fork == false
runs-on: ubuntu-latest
# The public interface should then allow the user to browse the cryptol
# documentation at the master branch, but also the documentation associated
Expand Down

0 comments on commit 5bbc3dc

Please sign in to comment.