diff options
| author | Enrico Tassi | 2020-11-23 12:08:22 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-11-27 14:29:22 +0100 |
| commit | d309974601ccb55f2339a4ea12d72428402ed195 (patch) | |
| tree | 9984462b0f8fc041c822d267efa7aba696068bdc /dev/doc | |
| parent | 7f3c46acc937eb9257c29b5881e5a8b17b28cd48 (diff) | |
[RM] script to notify "platform" projects to tag
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/release-process.md | 3 |
1 files changed, 3 insertions, 0 deletions
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 |