aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto3/Makefile
diff options
context:
space:
mode:
authorYves Bertot2019-01-11 09:16:48 +0100
committerGitHub2019-01-11 09:16:48 +0100
commitac8c25a9fac51745f0b53162fba48ef5b86d227d (patch)
treef7adb36b9519b9f957cca241767288518da70328 /doc/plugin_tutorial/tuto3/Makefile
parent44d767bc5f0f32d5bd7761e81ef225d96ab117b7 (diff)
parentcb2ee2d949899a897022894b750afd1f3d2eb478 (diff)
Merge pull request #8778 from SkySkimmer/merge-plugin-tuto
Move plugin tutorial to Coq repo
Diffstat (limited to 'doc/plugin_tutorial/tuto3/Makefile')
-rw-r--r--doc/plugin_tutorial/tuto3/Makefile14
1 files changed, 14 insertions, 0 deletions
diff --git a/doc/plugin_tutorial/tuto3/Makefile b/doc/plugin_tutorial/tuto3/Makefile
new file mode 100644
index 0000000000..e0e197650d
--- /dev/null
+++ b/doc/plugin_tutorial/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