diff options
| author | Gaëtan Gilbert | 2018-05-07 13:16:41 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-05-07 13:16:41 +0200 |
| commit | bb974290e7d05f1b1159c3add9f68f923ab4e1c4 (patch) | |
| tree | e4a0b3024ffb94c20ebe1bf48d7e70f544761c9e /dev/ci/docker/bionic_coq | |
| parent | 401e278be6e1f95d1175c5bcb1e33674074988dd (diff) | |
| parent | b0cd4a2db46f8051ffdf9001f3f9e894aa0b5b25 (diff) | |
Merge PR #7440: [ci] Add a default target to `Makefile.ci`
Diffstat (limited to 'dev/ci/docker/bionic_coq')
0 files changed, 0 insertions, 0 deletions