From 39861a12445742b481496baf2caafeb391773aba Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 21 Jun 2016 19:34:51 +0200 Subject: Makefile: compat5* moved in grammar/, less -I given to camlp4o --- dev/doc/build-system.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev') 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 -- cgit v1.2.3