From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 5 Mar 2008 10:18:51 +0000 (+0000)
Subject: verbosity increased in case of error
X-Git-Tag: make_still_working~5566
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=9f2c21d0360979096999aaecd5265cc12ac86fef;p=helm.git

verbosity increased in case of error
---

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 630b51be8..9c6c53aee 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -169,7 +169,8 @@ let add_single_obj uri obj refinement_toolkit =
         (* EXPERIMENTAL: pretty print the object in natural language *)
 	(try !object_declaration_hook uri obj
 	 with exc ->
-	  prerr_endline "Error: object_declaration_hook failed");
+	  prerr_endline ("Error: object_declaration_hook failed"^
+          Printexc.to_string exc));
         try 
          HLog.message
           (Printf.sprintf "%s defined" (UriManager.string_of_uri uri))