From a353fd786f4f75f94f7a5a7f78342c5ba6d810c6 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 15 Jan 2009 20:09:37 +0000
Subject: 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
---
 tools/coqdoc/main.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 65e2045a15..f187ae50db 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
 
-- 
cgit v1.2.3