Push updated documentation through CI jobs #636
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Support updating the documentation directly from GitHub Actions. Currently, the doc
Makefile
already uses the current Git branch (or tag) to define the version of the code (added in #606).This PR adds the necessary plumbing to push the documentation just built to the website's repository. In order to do so, we need the following:
[update-doc]
"The documentation is added to the website in a sub-folder with the same name as the branch, so that we can preview the documentation in a PR for review purposes. In between PRs, we may want to remove commits for these temporary branches from the website repository to avoid growing its size too much.
When pushing to
master
, Doxygen updates are pushed in addition to the manual.I have already verified that the website was correctly updated by generating pages like this:
https://colvars.github.io/push-doc/colvars-refman-namd.html
Will now delete those files from the website repository before attempting to merge into
master
.