From 78194cfd41178aaf8524b746a961d8a82363a234 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?=
 <129742207+bclement-ocp@users.noreply.github.com>
Date: Mon, 18 Sep 2023 13:34:06 +0000
Subject: [PATCH] Use `dune-release publish distrib` in `CONTRIBUTING.md`
 (#825)

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)