aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 2aa278c8e5..e1c7a87ee6 100644
--- a/Makefile
+++ b/Makefile
@@ -1254,8 +1254,8 @@ install-opt::
install-tools::
$(MKDIR) $(FULLBINDIR)
# recopie des fichiers de style pour coqide
- $(MKDIR) $(COQLIB)/tools/coqdoc
- cp tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(COQLIB)/tools/coqdoc
+ $(MKDIR) $(FULLCOQLIB)/tools/coqdoc
+ cp tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
cp $(TOOLS) $(FULLBINDIR)
LIBFILES=$(THEORIESVO) $(CONTRIBVO)