diff --git a/.github/workflows/CleanPreview.yml b/.github/workflows/CleanPreview.yml index 1710f50..96b7021 100644 --- a/.github/workflows/CleanPreview.yml +++ b/.github/workflows/CleanPreview.yml @@ -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 diff --git a/docs/make.jl b/docs/make.jl index 4b4cdd1..8ce493a 100644 --- a/docs/make.jl +++ b/docs/make.jl @@ -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 )