diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-24 18:37:24 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-24 18:37:24 +0100 |
| commit | 1d933c489d1f9d064fd54a4487754a86a0aed506 (patch) | |
| tree | 14ecb62f587e132c168383f5cae2e05314a543e7 /Makefile.common | |
| parent | 67319cef77a215163032ea94f28f8c21dcf64f3a (diff) | |
Revert "Makefile: the initial build of grammar.cma is now directory-driven"
This reverts commit f694544d016b085b3cd10007b9f7716ae2c3b022.
This commit was wrong, since (at least) the highparsing part depends
on the toplevel directory. I still didn't had time to fix that, so
in the meantime let's revert it.
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/Makefile.common b/Makefile.common index 41b45d97e..7425d99af 100644 --- a/Makefile.common +++ b/Makefile.common @@ -59,21 +59,16 @@ COQBINARIES:= $(COQMKTOP) \ CSDPCERT:=plugins/micromega/csdpcert$(EXE) -# Minimal set of source directories for building grammar.cma -# Invariant: the .ml4 there shouldn't use grammar.cma -# (the grammar-dependent .ml4 are in tactics, toplevel, plugins) -GRAMSRCDIRS:=\ - config lib intf kernel kernel/byterun library \ - pretyping interp proofs parsing grammar - -CORESRCDIRS:= $(GRAMSRCDIRS) printing tactics toplevel +CORESRCDIRS:=\ + config lib kernel kernel/byterun library \ + proofs tactics pretyping interp toplevel \ + parsing printing grammar intf PLUGINS:=\ omega romega micromega quote \ setoid_ring xml extraction fourier \ cc funind firstorder Derive \ - rtauto nsatz syntax decl_mode \ - btauto + rtauto nsatz syntax decl_mode btauto SRCDIRS:=\ $(CORESRCDIRS) \ |