diff options
| author | Enrico Tassi | 2017-08-04 16:51:30 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2017-08-04 16:51:30 +0200 |
| commit | 7a14df13a771651973da980eb9ab5c6608ffdcef (patch) | |
| tree | a7d26c7642f65c599b4ea6ea8800ff8bce85d2a9 /Makefile.install | |
| parent | 1f46ff6db53c2ca471d9ea067d0824755b2f34da (diff) | |
Makefile: install-byte works even if -coqide no
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 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/ |