diff options
| author | Maxime Dénès | 2017-08-16 09:41:53 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-16 09:41:53 +0200 |
| commit | ae827f670d8ea405ed06b52ad841cf690ebd18a8 (patch) | |
| tree | 42f2cc914fa780416cc095e0b335c68c8eccabd6 /Makefile.install | |
| parent | ffd6a20eb807cdd381d511e7b59799495122591d (diff) | |
| parent | 7a14df13a771651973da980eb9ab5c6608ffdcef (diff) | |
Merge PR #951: 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/ |