aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.ide
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-08-04 16:51:30 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-08-04 16:51:30 +0200
commit7a14df13a771651973da980eb9ab5c6608ffdcef (patch)
treea7d26c7642f65c599b4ea6ea8800ff8bce85d2a9 /Makefile.ide
parent1f46ff6db53c2ca471d9ea067d0824755b2f34da (diff)
Makefile: install-byte works even if -coqide no
Diffstat (limited to 'Makefile.ide')
-rw-r--r--Makefile.ide13
1 files changed, 10 insertions, 3 deletions
diff --git a/Makefile.ide b/Makefile.ide
index b534b385b..ecfe92cc5 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -127,21 +127,24 @@ ide/%.cmx: ide/%.ml
## Install targets
####################
-.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles install-ide-byte
+.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles install-ide-byte install-ide-toploop-byte install-coqide-byte
ifeq ($(HASCOQIDE),no)
install-coqide: install-ide-toploop
else
install-coqide: install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
endif
+ifeq ($(HASCOQIDE),no)
+install-coqide-byte: install-ide-toploop-byte
+else
+install-coqide-byte: install-ide-toploop-byte install-ide-byte
+endif
# Apparently, coqide.byte is not meant to be installed
install-ide-byte:
$(MKDIR) $(FULLCOQLIB)
$(INSTALLSH) $(FULLCOQLIB) $(IDECMA)
- $(MKDIR) $(FULLCOQLIB)/toploop
- $(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/
install-ide-bin:
$(MKDIR) $(FULLBINDIR)
@@ -151,6 +154,10 @@ install-ide-toploop:
ifeq ($(BEST),opt)
$(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
endif
+install-ide-toploop-byte:
+ifneq ($(BEST),opt)
+ $(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/
+endif
install-ide-devfiles:
$(MKDIR) $(FULLCOQLIB)