aboutsummaryrefslogtreecommitdiff
path: root/dev/tools/pin-ci.sh
AgeCommit message (Collapse)Author
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.