Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Use
dune-release publish distrib
in CONTRIBUTING.md
Otherwise, `dune-release publish` also publishes the doc to GitHub pages, but we currently manage the GitHub pages from the CI with additional informations.
- Loading branch information