Correctly post GitHub commit status for out-of-repo deployment#2816

fingolfin merged 3 commits intoJuliaDocs:masterJuliaDocs/Documenter.jl:masterfrom

giordano:mg/post-github-status-deploydocgiordano/Documenter.jl:mg/post-github-status-deploydocCopy head branch name to clipboard