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