diff options
| -rw-r--r-- | Makefile.build | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/Makefile.build b/Makefile.build index f1278770d5..2a9986d10e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -333,19 +333,15 @@ $(COQIDEBYTE): $(LINKIDE) | $(COQTOPBYTE) .PHONY: install-coqide install-ide-no install-ide-byte install-ide-opt .PHONY: install-ide-files install-ide-info install-im install-ide-devfiles -install-coqide:: install-ide-$(HASCOQIDE) install-ide-files install-ide-info install-ide-devfiles - -install-ide-no: - -install-ide-byte: - $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQIDEBYTE) $(FULLBINDIR) - cd $(FULLBINDIR); ln -sf coqide.byte$(EXE) coqide$(EXE) +ifeq ($(HASCOQIDE),no) +install-coqide: +else +install-coqide: install-ide-bin install-ide-files install-ide-info install-ide-devfiles +endif -install-ide-opt: +install-ide-bin: $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQIDEOPT) $(FULLBINDIR) - cd $(FULLBINDIR); ln -sf coqide.opt$(EXE) coqide$(EXE) + $(INSTALLBIN) $(COQIDE) $(FULLBINDIR) install-ide-devfiles: $(MKDIR) $(FULLCOQLIB) |