aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdoc/main.ml10
1 files changed, 10 insertions, 0 deletions
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 865f101f60..f81a3b78b0 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -419,6 +419,16 @@ 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 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 dst = if !output_dir <> "" then
+ Filename.concat !output_dir "coqdoc.sty"
+ else "coqdoc.sty" in
+ copy src dst);
match !out_to with
| StdOut ->
Cdglobals.out_channel := stdout;