From 7fcfef1d6efabfb0c736621499c342d060856499 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 28 Nov 2019 18:06:10 +0100
Subject: Add a script to pin CI developments.

It is useful for the release process, and there is no reason for somebody
to lose time reimplementing it again.
---
 dev/doc/release-process.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'dev/doc/release-process.md')

diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 1c486b024d..ba68501e04 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -75,7 +75,8 @@ in time.
 - [ ] Pin the versions of libraries and plugins in
   `dev/ci/ci-basic-overlays.sh` to use commit hashes or tag (or, if it
   exists, a branch dedicated to compatibility with the corresponding
-  Coq branch).
+  Coq branch). You can use the `dev/tools/pin-ci.sh` script to do this
+  semi-automatically.
 - [ ] Remove all remaining unmerged feature PRs from the beta milestone.
 - [ ] Start a new project to track PR backporting. The project should
   have a "Request X.X+beta1 inclusion" column for the PRs that were
-- 
cgit v1.2.3