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 /dev/doc/build-system.txt | |
| parent | a1a86e6572bbae9e515cc72d7072322e5a11b49e (diff) | |
Makefile: compat5* moved in grammar/, less -I given to camlp4o
Diffstat (limited to 'dev/doc/build-system.txt')
| -rw-r--r-- | dev/doc/build-system.txt | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index 4593a6ad5..873adc1b2 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -117,7 +117,7 @@ Targets for cleaning various parts: --------------- There is now two kinds of preprocessed files : - - a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp) + - a .mlp do not need grammar.cma (they are in grammar/) - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo), except coqide_main.ml4 and its specific rule |