diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-15 20:09:37 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-15 20:09:37 +0000 |
| commit | a353fd786f4f75f94f7a5a7f78342c5ba6d810c6 (patch) | |
| tree | c0603fae83adc02000876cecc756a67f10c5a4a9 /tools/coqdoc/main.ml | |
| parent | 511cb2f5f42d80af9262b5cf7458a434cd652e95 (diff) | |
Patch by Brian Campbell to output more information on the exception that
made a glob file unreadable.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11788 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/main.ml')
| -rw-r--r-- | tools/coqdoc/main.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 65e2045a1..f187ae50d 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -426,10 +426,10 @@ let read_glob x = match x with | Vernac_file (f,m) -> let glob = (Filename.chop_extension f) ^ ".glob" in - (try + (try Vernac_file (f, Index.read_glob glob) - with _ -> - eprintf "Warning: file %s cannot be opened; links will not be available\n" glob; + with e -> + eprintf "Warning: file %s cannot be used; links will not be available: %s\n" glob (Printexc.to_string e); x) | Latex_file _ -> x |