diff options
| author | Emilio Jesus Gallego Arias | 2018-05-06 14:46:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-05-06 14:56:22 +0200 |
| commit | b0cd4a2db46f8051ffdf9001f3f9e894aa0b5b25 (patch) | |
| tree | f31dca1bcca6b2c9fb3df6a6c1e8dc9f23624d7f /dev/ci/docker/bionic_coq | |
| parent | 87c959542e1bed55b14d371f1be02cd60d89082c (diff) | |
[ci] Add a default target to `Makefile.ci`
So we avoid problems like the one in #7438.
Diffstat (limited to 'dev/ci/docker/bionic_coq')
0 files changed, 0 insertions, 0 deletions