aboutsummaryrefslogtreecommitdiff
path: root/dev/tools/pin-ci.sh
AgeCommit message (Collapse)Author
2020-12-14Update dev/tools/pin-ci.shEnrico Tassi
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-12-14[ci] simplify script to pin ci projectsEnrico Tassi
2019-12-02Add 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.