aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-01-07 14:26:24 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-01-07 14:26:24 +0000
commitde291a7cf681d0b7107946fa33bc0b524c46c1f2 (patch)
tree0e503387b1057ea8d1c4870d5107727eb24b613c
parentacc841a5c88c7a6c5876301c96dffe2f8114d131 (diff)
Don't install both coqide.byte and coqide.opt
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13776 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile.build2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build
index d75051b20..e6227aea6 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)