aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-05-02 10:14:39 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-05-02 10:14:39 +0000
commit8a02b7d87eccf51893f13764841e833fae6079d1 (patch)
tree2d8b0ee3000cbf6b6f68c46af8b48bcb3c8400c9 /tools
parent8e6b8c82ea3b7b4afe9ad770f34c98359f71fb9a (diff)
Option --coqlib_path pour coqdoc (suite et fin)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8777 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdoc/main.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 892104340..90b15b64d 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -425,11 +425,11 @@ let index_module = function
let produce_document l =
List.iter index_module l;
(if !target_language=HTML then
- let src = (Filename.concat Coq_config.coqlib "/tools/coqdoc/coqdoc.css") in
+ let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in
let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.css" else "coqdoc.css" in
copy src dst);
(if !target_language=LaTeX then
- let src = (Filename.concat Coq_config.coqlib "/tools/coqdoc/coqdoc.sty") in
+ let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in
let dst = if !output_dir <> "" then
Filename.concat !output_dir "coqdoc.sty"
else "coqdoc.sty" in