diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-07-25 17:05:41 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-07-25 17:05:50 +0200 |
| commit | 9d8ac85003706b7c436d3e8b1d31b3baadae47c6 (patch) | |
| tree | 6a7d31713e232929390f48c094361d095d5ea9e5 /Makefile.ide | |
| parent | c0fdb912c5e63bb43d6e8dd320e9f5613c6237ff (diff) | |
Makefile.ide: restore a coqide-binaries rule (fix bug 5667)
This rule is used by opam package coq-coqide
Diffstat (limited to 'Makefile.ide')
| -rw-r--r-- | Makefile.ide | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/Makefile.ide b/Makefile.ide index 0cfbdeb4e..b534b385b 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -61,12 +61,16 @@ GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0) # CoqIde special targets ########################################################################### -.PHONY: coqide coqide-opt coqide-byte coqide-files +.PHONY: coqide coqide-opt coqide-byte coqide-files coqide-binaries .PHONY: ide-toploop ide-byteloop ide-optloop -# target to build CoqIde +# target to build CoqIde (native version) and the stuff needed to lauch it coqide: coqide-files coqide-opt theories/Init/Prelude.vo +# target to build CoqIde (in native and byte versions), and no more +# NB: this target is used in the opam package coq-coqide +coqide-binaries: coqide-opt coqide-byte + ifeq ($(HASCOQIDE),opt) coqide-opt: $(COQIDE) ide-toploop else |