diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-21 19:34:51 +0200 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-21 20:35:36 +0200 |
commit | 39861a12445742b481496baf2caafeb391773aba (patch) | |
tree | 8e38399836572cf13947d28c4ebd6eb4e2ca4240 /Makefile.common | |
parent | a1a86e6572bbae9e515cc72d7072322e5a11b49e (diff) |
Makefile: compat5* moved in grammar/, less -I given to camlp4o
Diffstat (limited to 'Makefile.common')
-rw-r--r-- | Makefile.common | 2 |
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 |