diff options
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index d75051b20c..e6227aea61 100644 --- a/Makefile.build +++ b/Makefile.build @@ -337,7 +337,7 @@ install-ide-byte: install-ide-opt: $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQIDEBYTE) $(COQIDEOPT) $(FULLBINDIR) + $(INSTALLBIN) $(COQIDEOPT) $(FULLBINDIR) $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a) \ `cat $(IDECMA:.cma=.mllib.d) | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.cmi/p"` cd $(FULLBINDIR); ln -sf coqide.opt$(EXE) coqide$(EXE) |