X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMisc.ml;h=2112952610869c0495575a7f1bb5a75948cd5d6c;hb=10f29fdd78ee089a9a94446207b543d33d6c851c;hp=0c4329e554350936ea863f1c2e581e13df8ca5d9;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/matita/matitaMisc.ml b/helm/software/matita/matitaMisc.ml
index 0c4329e55..211295261 100644
--- a/helm/software/matita/matitaMisc.ml
+++ b/helm/software/matita/matitaMisc.ml
@@ -30,7 +30,10 @@ open Printf
 (** Functions "imported" from Http_getter_misc *)
 
 let normalize_dir = Http_getter_misc.normalize_dir
-let strip_suffix = Http_getter_misc.strip_suffix
+let strip_suffix ~suffix s = 
+  try 
+    Http_getter_misc.strip_suffix ~suffix s
+  with Invalid_argument _ -> s
 
 let absolute_path file =
   if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file
@@ -150,3 +153,11 @@ let list_tl_at ?(equality=(==)) e l =
     | hd :: tl -> aux tl
   in
   aux l
+
+let shutup () = 
+  HLog.set_log_callback (fun _ _ -> ());
+(*
+  let out = open_out "/dev/null" in
+  Unix.dup2 (Unix.descr_of_out_channel out) (Unix.descr_of_out_channel stderr)
+*)
+