diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -81,7 +81,7 @@ DEPFLAGS=$(LOCALINCLUDES) OCAMLC_P4O=$(OCAMLC) -pp $(CAMLP4O) $(BYTEFLAGS) OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS) CAMLP4EXTENDFLAGS=-I . pa_extend.cmo pa_extend_m.cmo q_MLast.cmo -CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$$|\1|p' +CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)|\1|p' COQINCLUDES= # coqtop includes itself the needed paths GLOB= # is "-dump-glob file" when making the doc |