Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
This is the PR-actionable part of #157 (comment). Note that extra actions are needed to be done by the maintainer of the repository to ensure that the result of the github actions determine the content of gh-pages.
- Loading branch information