aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile3
1 files changed, 3 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 385d8322e4..2e2eef1bf7 100644
--- a/Makefile
+++ b/Makefile
@@ -1243,6 +1243,9 @@ 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
cp $(TOOLS) $(FULLBINDIR)
LIBFILES=$(THEORIESVO) $(CONTRIBVO)