diff options
| author | Pierre-Marie Pédrot | 2018-11-21 19:16:42 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-21 19:16:42 +0100 |
| commit | 5d3e09970635c68e993ed12fd3313fd2702915fa (patch) | |
| tree | 61c06dcb7313b989bcc42aebf23d0b0cd2465e49 /Makefile.ide | |
| parent | 452cb15fd9647dc453cc36614cc469dfa91e3080 (diff) | |
| parent | aa151dbc7aa501bac78b835a80f9a25c5316d2dc (diff) | |
Merge PR #8945: [camlp5] Remove dependency on camlp5.
Diffstat (limited to 'Makefile.ide')
| -rw-r--r-- | Makefile.ide | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.ide b/Makefile.ide index 39af1f8545..cae77ee348 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -147,7 +147,7 @@ $(IDETOPEXE): $(IDETOP:.opt=.$(BEST)) $(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \ - $(SYSMOD) -package camlp5.gramlib \ + $(SYSMOD) \ $(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@ $(STRIP_HIDE) $@ $(CODESIGN_HIDE) $@ @@ -156,7 +156,7 @@ $(IDETOPBYTE): ide/idetop.ml $(LINKCMO) $(LIBCOQRUN) $(IDETOPCMA) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \ -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \ - $(SYSMOD) -package camlp5.gramlib \ + $(SYSMOD) \ $(LINKCMO) $(IDETOPCMA) $(BYTEFLAGS) $< -o $@ #################### |