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 --- Makefile.ide | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile.ide') diff --git a/Makefile.ide b/Makefile.ide index c50e42341..21821bfea 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -96,7 +96,7 @@ $(COQIDEBYTE): $(LINKIDE) ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@ + $(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@ ide/%.cmi: ide/%.mli -- cgit v1.2.3