aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile.build1
1 files changed, 0 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build
index 559d0f378e..ef2bb067d3 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -338,7 +338,6 @@ install-ide-files:
$(MKDIR) $(FULLDATADIR)
$(INSTALLLIB) ide/coq.png $(FULLDATADIR)
$(MKDIR) $(FULLCONFIGDIR)
- $(INSTALLLIB) $(FULLCONFIGDIR)
if [ $(IDEOPTINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi
install-ide-info: