aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-21 19:34:51 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-21 20:35:36 +0200
commit39861a12445742b481496baf2caafeb391773aba (patch)
tree8e38399836572cf13947d28c4ebd6eb4e2ca4240 /Makefile.common
parenta1a86e6572bbae9e515cc72d7072322e5a11b49e (diff)
Makefile: compat5* moved in grammar/, less -I given to camlp4o
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common
index e156b101c..310e30a0c 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -88,7 +88,7 @@ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
-GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma
+GRAMMARCMA:=grammar/compat5.cmo grammar/grammar.cma
# modules known by the toplevel of Coq