diff options
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 |