From 62bc367dbd71622ce035722efaaa04bac0fa2b40 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Mon, 18 Sep 2023 15:10:08 +0200 Subject: [PATCH] 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. --- CONTRIBUTING.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 9ad001d38..49a79b248 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -99,6 +99,6 @@ The release is made using `dune-release`, and follows standard procedure for the - `dune-release check` (performs basic check) - `dune-release tag vX.Y.Z` (replace `X`, `Y` and `Z` as appropriate; this creates a git tag -- you may add alphas, betas, or rc) - `dune-release distrib` (this creates the distribution archive) - - `dune-release publish` (this is irreversible: it publishes the release on GitHub) + - `dune-release publish distrib` (this is irreversible: it publishes the release on GitHub) - `dune-release opam pkg` (this an archive with the opam stuff) - `dune-release opam submit` (this opens a MR on the opam repository)