Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
The git checkout command was in the continuous deployment script in order to get the correct information to go in the footer of the PDF. However, since the build is happening on the basis of a tag, the git repository was in a detached HEAD state, meaning that the branch information that showed up in the footer of the PDF was 'origin/HEAD', rather than 'master'. To fix this, the script now runs `git checkout master` instead of `git checkout`. This solution is a bit hacky because, in principle, the tag that is being built might be a different commit than the most recent commit on the master branch. However, it should work well enough for now, but it would be nice to have a more robust solution in the future.
- Loading branch information