diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-02 15:57:17 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-02 15:57:17 +0000 |
| commit | 62aa6ad82ed5d986da1b979296a82fb46e64b55d (patch) | |
| tree | ada6cd0efb5436f1c03e0c4b8f2649b625838187 | |
| parent | 0c77c34291ce7d699456b21b07b0ecf2cb366c31 (diff) | |
New makefile shortcuts miniopt and minibyte for coqtop + plugins
They are meant to quickly check that all the ml code of coqtop
and its plugins is compilable
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15841 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.build | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index 41d0fc18a..7a1058f10 100644 --- a/Makefile.build +++ b/Makefile.build @@ -206,6 +206,9 @@ coqlight: theories-light tools coqbinaries states: theories/Init/Prelude.vo +miniopt: $(COQTOPEXE) pluginsopt +minibyte: $(COQTOPBYTE) pluginsbyte + ifeq ($(BEST),opt) $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' @@ -442,7 +445,7 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \ ########################################################################### .PHONY: plugins omega micromega setoid_ring nsatz xml extraction -.PHONY: fourier funind cc rtauto btauto pluginsopt +.PHONY: fourier funind cc rtauto btauto pluginsopt pluginsbyte plugins: $(PLUGINSVO) omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA) @@ -458,6 +461,7 @@ rtauto: $(RTAUTOVO) $(RTAUTOCMA) btauto: $(BTAUTOVO) $(BTAUTOCMA) pluginsopt: $(PLUGINSOPT) +pluginsbyte: $(PLUGINS) ########################################################################### # rules to make theories and plugins |