aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/main.ml
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-02-25 17:38:03 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-02-25 17:38:03 +0000
commit86247a9360e2b87442d59e883aa9fd39796682f1 (patch)
treed177cbb8b829d86d65d82e350ad2ec52c97d9cec /tools/coqdoc/main.ml
parent0d56cbb9acb4d66e24327918bdc50567a903354e (diff)
Correction d'un bug de Coqdoc (indentation des lignes)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10583 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/main.ml')
-rw-r--r--tools/coqdoc/main.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 5744f4d6e..2998e8c25 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -435,11 +435,11 @@ let produce_document l =
copy src dst;
List.iter read_glob l);
(if !target_language=LaTeX then
- 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
- copy src dst);
+ 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
+ copy src dst);
List.iter index_module l;
match !out_to with
| StdOut ->