diff options
| author | coqbot-app[bot] | 2020-11-27 15:29:58 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-27 15:29:58 +0000 |
| commit | f733414e59afb37cad41c65b11bc4c817bd137f9 (patch) | |
| tree | 3d4ae12824d331a404443507df80e79b69cb0355 /dev/doc | |
| parent | 2a21e55ead07a0f1c23e78c88ab6c8f9acb56c91 (diff) | |
| parent | d309974601ccb55f2339a4ea12d72428402ed195 (diff) | |
Merge PR #13449: [RM] script to notify "platform" projects to tag
Reviewed-by: Zimmi48
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 |