From 7a14df13a771651973da980eb9ab5c6608ffdcef Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 4 Aug 2017 16:51:30 +0200
Subject: Makefile: install-byte works even if -coqide no

---
 Makefile.install | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.install')

diff --git a/Makefile.install b/Makefile.install
index 02ae724dfe..85ffc93d51 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -74,7 +74,7 @@ ifeq ($(BEST),opt)
 	$(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
 endif
 
-install-byte: install-ide-byte
+install-byte: install-coqide-byte
 	$(MKDIR) $(FULLBINDIR)
 	$(INSTALLBIN) $(COQTOPBYTE) $(FULLBINDIR)
 	$(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/
-- 
cgit v1.2.3