diff options
Diffstat (limited to 'Makefile.install')
| -rw-r--r-- | Makefile.install | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.install b/Makefile.install index 02ae724df..85ffc93d5 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/ |