Skip to content

Commit

Permalink
Disable documentation previews (#11)
Browse files Browse the repository at this point in the history
While this now deletes old previews when the PR closes,
presumably they still add to the git history and thus
the size of the repo. This disables them for now.
  • Loading branch information
timholy authored Oct 12, 2023
1 parent 07df3a7 commit 45cf56e
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 1 deletion.
1 change: 1 addition & 0 deletions .github/workflows/CleanPreview.yml
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ on:

jobs:
doc-preview-cleanup:
if: false # disable this workflow (change if `push_preview=true` in make.jl)
runs-on: ubuntu-latest
permissions:
contents: write
Expand Down
2 changes: 1 addition & 1 deletion docs/make.jl
Original file line number Diff line number Diff line change
Expand Up @@ -27,5 +27,5 @@ makedocs(;
deploydocs(;
repo="github.com/timholy/ThickNumbers.jl",
devbranch="main",
push_preview=true,
push_preview=false, # see also the corresponding flag in .github/workflows/CleanPreview.yml
)

0 comments on commit 45cf56e

Please sign in to comment.