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