From d309974601ccb55f2339a4ea12d72428402ed195 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 Nov 2020 12:08:22 +0100
Subject: [RM] script to notify "platform" projects to tag

---
 dev/doc/release-process.md | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'dev/doc')

diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index da9f37f666..9b43bddd86 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -80,6 +80,9 @@ in time.
   exists, a branch dedicated to compatibility with the corresponding
   Coq branch). You can use the `dev/tools/pin-ci.sh` script to do this
   semi-automatically.
+  - [ ] Notify upstream authors about the pinning, see
+    `dev/tools/notify-upstream-pins.sh`. As of today there is no automated
+    way to track these issues.
 - [ ] 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