It looks like the documentation is no longer being built — when @timholy switched to Github CI (#51) from Travis, did we forget to port over the doc building from Travis?
Also, while I'm updating these scripts, we can drop our ancient support for Julia 0.7, which no one cares about anymore. Also updated the TagBot script to the latest recommended script since we had to add the DOCUMENTER_KEY to that anyway.
It looks like the documentation is no longer being built — when @timholy switched to Github CI (#51) from Travis, did we forget to port over the doc building from Travis?
Also, while I'm updating these scripts, we can drop our ancient support for Julia 0.7, which no one cares about anymore. Also updated the TagBot script to the latest recommended script since we had to add the DOCUMENTER_KEY to that anyway.