aboutsummaryrefslogtreecommitdiff
path: root/Makefile.dev
diff options
context:
space:
mode:
authorMaxime Dénès2017-05-17 09:35:06 +0200
committerMaxime Dénès2017-05-17 09:35:06 +0200
commit4b53985c2888827fe030294f95b5975d5e34e4c7 (patch)
treefc01eb8a20ebe09abe73a2707d53f0393b8f8ceb /Makefile.dev
parent772de8aba675731ed8d476ea0bc628ee21751dc8 (diff)
parentd8d56dfadc571fdf23ff9f8cb97d4c8cd96691ee (diff)
Merge PR#614: Improve Travis
Diffstat (limited to 'Makefile.dev')
-rw-r--r--Makefile.dev5
1 files changed, 4 insertions, 1 deletions
diff --git a/Makefile.dev b/Makefile.dev
index 5931e46dd0..1803cc8ffe 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -97,7 +97,10 @@ minibyte: $(COQTOPBYTE) pluginsbyte
pluginsopt: $(PLUGINSOPT)
pluginsbyte: $(PLUGINS)
-.PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte
+# This should build all the ocaml code but not (most of) the .v files
+coqocaml: tools coqbinaries pluginsopt coqide printers
+
+.PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte coqocaml
##########################
### 2) core ML components