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