aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-09-18 13:42:19 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-09-18 13:42:19 +0000
commitb0e06c6033141318896423054dfbe1e0144cd5ab (patch)
tree2ad75f4dd15b62df22bbae2c41725984ea4a61c8 /Makefile
parentd35116074a4431e95129141ef8883b5169c16b63 (diff)
Correction du bug #1215
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9149 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile3
1 files changed, 3 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 385d8322e..2e2eef1bf 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)