| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-12-14 | Update dev/tools/pin-ci.sh | Enrico Tassi | |
| Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
| 2020-12-14 | [ci] simplify script to pin ci projects | Enrico Tassi | |
| 2019-12-02 | Add a script to pin CI developments. | Pierre-Marie Pédrot | |
| It is useful for the release process, and there is no reason for somebody to lose time reimplementing it again. | |||
