Documenter devbranch build not deploying

[mortenpi]

Documenter predates workflow_dispatch, so yeah, deploydocs just doesn’t know what do with it. But I think we should support it, although I am not sure whether it should be exactly equivalent to push or not.

@miles

if I change it to “push”, will that break other ways that this action gets run (e.g. manually running it versus it running as part of our continuous integration on PR’s)?

It should be completely fine if you do something like

if get(ENV, "GITHUB_EVENT_NAME", nothing) == "workflow_dispatch"
    ENV["GITHUB_EVENT_NAME"] = "push"
end

just before deploydocs.