Documenter

gitrm_copy(src, dst)

Uses git rm -r to remove dst and then copies src to dst. Assumes that the working directory is within the git repository of dst is when the function is called.

This is to get around #507 on filesystems that are case-insensitive (e.g. on OS X, Windows). Without doing a git rm first, git add -A will not detect case changes in filenames.

git_push(
    root, tmp, repo;
    branch="gh-pages", dirname="", target="site", tag="", key="", sha="", devurl="dev"
)

Handles pushing changes to the remote documentation branch. When tag is empty the docs are deployed to the devurl directory, and when building docs for a tag they are deployed to a vX.Y.Z directory.