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 /Makefile.ide | |
| parent | a1a86e6572bbae9e515cc72d7072322e5a11b49e (diff) | |
Makefile: compat5* moved in grammar/, less -I given to camlp4o
Diffstat (limited to 'Makefile.ide')
| -rw-r--r-- | Makefile.ide | 2 |
1 files changed, 1 insertions, 1 deletions
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 |