diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-29 11:59:11 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-29 11:59:11 +0000 |
| commit | 62ddbf4c06974bb701dd6b370c6b4d670cb5d7cd (patch) | |
| tree | e4d7d609af1b03ffa12b7c7c0ce4e08ea06303ca /tools/coqdoc/main.ml | |
| parent | 97da8221e0097ed365f0a99e4960148424a59734 (diff) | |
Added checksums to glob files and warned about possibly missing
packages for utf8.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14623 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/main.ml')
| -rw-r--r-- | tools/coqdoc/main.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 7dc2c3bf2..b1303f18f 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -447,13 +447,13 @@ 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_file x = - try Index.read_glob x - with Sys_error s -> - eprintf "Warning: %s (links will not be available)\n" s +let read_glob_file vfile f = + try Index.read_glob vfile f + with Sys_error s -> eprintf "Warning: %s (links will not be available)\n" s let read_glob_file_of = function - | Vernac_file (f,_) -> read_glob_file (Filename.chop_extension f ^ ".glob") + | Vernac_file (f,_) -> + read_glob_file (Some f) (Filename.chop_extension f ^ ".glob") | Latex_file _ -> () let index_module = function @@ -475,7 +475,7 @@ let produce_document l = (match !Cdglobals.glob_source with | NoGlob -> () | DotGlob -> List.iter read_glob_file_of l - | GlobFile f -> read_glob_file f); + | GlobFile f -> read_glob_file None f); List.iter index_module l; match !out_to with | StdOut -> |