diff options
author | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-13 16:41:50 +0000 |
---|---|---|
committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-13 16:41:50 +0000 |
commit | bc50989dea9a5bd1b4ec891e63d67fd3fd2f9c3e (patch) | |
tree | 1cfa9716f3e0b6f8148f88a1776fe776d12d39f3 /tools/coqdoc/main.ml | |
parent | ded46fc00ee76c3f2568619e1a48034b5865a8f2 (diff) |
Correction du bug #1512
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10562 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/main.ml')
-rw-r--r-- | tools/coqdoc/main.ml | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index c3a32f08f..a4653d9b7 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -421,28 +421,33 @@ let gen_mult_files l = end (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *) +let read_glob = function + | Vernac_file (f,m) -> + let glob = (Filename.chop_extension f) ^ ".glob" in + (try + Index.read_glob glob + with + _ -> eprintf "Warning: file %s cannot be opened; links will not be available\n" glob) + | Latex_file _ -> () -let glob_filename f = - (Filename.chop_extension f) ^ ".glob" - let index_module = function | Vernac_file (f,m) -> - Index.read_glob (glob_filename f); Index.add_module m | Latex_file _ -> () let produce_document l = - List.iter index_module l; (if !target_language=HTML then 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); + 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); + List.iter index_module l; match !out_to with | StdOut -> Cdglobals.out_channel := stdout; |