The Documenter log seems to suggest that setting push_preview=true is necessary when generating docs from a git-hub action, as here
Is this actually necessary?
1 Like
This is my understanding:
- If
push_previewistrue, pull request preview builds will be pushed, and builds onmasterwill also be pushed
Ifpush_previewisfalse, pull request preview builds will NOT be pushed, but builds onmasterWILL still be pushed
It would be good to get clarification from @mortenpi
Or @fredrikekre
Yep, what @dilumaluthge says is true.
But I think the issue here is that you want to build the development version docs when you push to the dev branch, right? In this case, you should set devbranch = "dev" in that case – deploydocs by default assumes it is called "master".
1 Like
If I understand correctly, we do NOT want to build the docs on pushes to the dev branch.
We DO want to build the docs on pushes to the master branch.
@ablaom Is that correct?
1 Like
Yes. Building docs for every PR slows things down, especially at MLJ.jl. So we have only generated docs for dev → master PRs
@dilumaluthge has worked out a solution to this for the ci.yml file and tested that indeed the make.jl file deploy command can drop the push_preview=true flag.
This ci.yml file can be viewed here, which is for workflows where most new PR’s are onto a dev branch and master is for tagged releases and doc-updates.
Many thanks to @dilumaluthge for this support and guiding us all through the travis → github/action transition 
2 Likes