diff options
| author | Gaëtan Gilbert | 2020-01-19 22:01:07 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-19 22:01:07 +0100 |
| commit | b2352a5025e290e4e0a00df162d05f95bcc0f05a (patch) | |
| tree | 76fb8f6d4779b4a74a713f5b7c94d8f41b41b6f7 /dev/dune | |
| parent | 2ae084f55c2e9bce3023a25a1e2c7a70dadcf348 (diff) | |
| parent | 7fcfef1d6efabfb0c736621499c342d060856499 (diff) | |
Merge PR #11214: Add a script to pin CI developments.
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Diffstat (limited to 'dev/dune')
0 files changed, 0 insertions, 0 deletions