diff options
| -rw-r--r-- | Makefile.ci | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.ci b/Makefile.ci index 0136852180..e778fe9190 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -7,4 +7,4 @@ CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \ # Generic rule, we use make to easy travis integraton with mixed rules $(CI_TARGETS): ci-%: - ./dev/ci/ci-$*.sh + +./dev/ci/ci-$*.sh |