diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-04 23:55:24 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-07 10:27:17 +0100 |
| commit | 138a4da7f0133d7b4ea06cfbc938d23ddb88c97d (patch) | |
| tree | 8f54418ccec857d9d5dea108ccaed0cf8de221de /Makefile.ci | |
| parent | 3a66f149a34613ef0ed04046fed3947e8e720cd6 (diff) | |
[travis] [External CI] Script renaming.
Diffstat (limited to 'Makefile.ci')
| -rw-r--r-- | Makefile.ci | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/Makefile.ci b/Makefile.ci new file mode 100644 index 000000000..ada698e0a --- /dev/null +++ b/Makefile.ci @@ -0,0 +1,13 @@ +.PHONY: ci-all ci-hott ci-math-comp ci-compcert + +ci-all: ci-hott ci-math-comp ci-compcert + +# TODO Do generic rule +ci-hott: + ./tools/ci/ci-hott.sh + +ci-math-comp: + ./tools/ci/ci-math-comp.sh + +ci-compcert: + ./tools/ci/ci-compcert.sh |