From 9d8ac85003706b7c436d3e8b1d31b3baadae47c6 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 25 Jul 2017 17:05:41 +0200 Subject: Makefile.ide: restore a coqide-binaries rule (fix bug 5667) This rule is used by opam package coq-coqide --- Makefile.ide | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'Makefile.ide') 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 -- cgit v1.2.3