diff options
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 |