diff options
| -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 |