diff options
| author | Pierre-Marie Pédrot | 2019-11-28 18:06:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-02 09:14:22 +0100 |
| commit | 7fcfef1d6efabfb0c736621499c342d060856499 (patch) | |
| tree | eebaa15a3cbf919c482c98f5fb9df21370ad37bd /dev/doc/release-process.md | |
| parent | 31e109671896ef42653b1fcf239d8ebe1424c3da (diff) | |
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.
Diffstat (limited to 'dev/doc/release-process.md')
| -rw-r--r-- | dev/doc/release-process.md | 3 |
1 files changed, 2 insertions, 1 deletions
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 |