X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMisc.ml;h=2112952610869c0495575a7f1bb5a75948cd5d6c;hb=25aa80d913c903fcc270d05464cf3084b12d52a8;hp=266aec526920ad8d96bda49f7cca4cd0d29a2861;hpb=aef659e5893b4bf8c8544d0c54714e10f5b5493a;p=helm.git diff --git a/helm/software/matita/matitaMisc.ml b/helm/software/matita/matitaMisc.ml index 266aec526..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 @@ -153,6 +156,8 @@ let list_tl_at ?(equality=(==)) e 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) +*)