aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorYves Bertot2018-05-09 11:00:42 +0200
committerYves Bertot2018-05-09 11:00:42 +0200
commitf30878bfd1e602fd793beb70b5b1fff8f0cc826e (patch)
treecf073b7665622d75a9061a6128ee3449eb48d940
parent9bd7f64e1a1d3d2b055a7df23d31f0ed76f28649 (diff)
makefile is necessary
-rw-r--r--tuto3/Makefile14
1 files changed, 14 insertions, 0 deletions
diff --git a/tuto3/Makefile b/tuto3/Makefile
new file mode 100644
index 0000000000..e0e197650d
--- /dev/null
+++ b/tuto3/Makefile
@@ -0,0 +1,14 @@
+ifeq "$(COQBIN)" ""
+ COQBIN=$(dir $(shell which coqtop))/
+endif
+
+%: Makefile.coq
+
+Makefile.coq: _CoqProject
+ $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
+
+tests: all
+ @$(MAKE) -C tests -s clean
+ @$(MAKE) -C tests -s all
+
+-include Makefile.coq