{subsection: Publishing the manual onto Read the Docs} *:: Currently Mark or Josh has to login to Read the Docs to manually push any changes. -*:: Before we go live in May 2019, we'll set up a webhook in our git repository. This will cause any changes to get pushed automatically. + +{subsection: Different versions of the manual} + +*:: To make changes to the devel/latest version of the manual, put all your changes in the master branch. +*:: To make changes to the stable version of the manual, you need to add a tag called "stable" to the commit in V8_8-branch that contains the changes you want. To update the stable tag to a new commit, run the following: +{code} +git tag --delete stable +git push --delete origin tag stable +git tag stable +git push origin stable +{endcode} {subsection: Generating man pages}