X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMisc.ml;h=ca8dc2446660ec11d5e424119f53be2ff4ebd6a4;hb=35d7685022202a24dac2d0cab17796b492a8d50d;hp=82a5a521e57173899b8d6201043b9f78a495b0a7;hpb=2d03016df7f68c81dd0f25bf18a792a80b412702;p=helm.git diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 82a5a521e..ca8dc2446 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -246,26 +246,7 @@ class ['a] browser_history ?memento size init = let singleton f = let instance = lazy (f ()) in fun () -> Lazy.force instance -(* -let mkdir d = - let errmsg = sprintf "Unable to create directory \"%s\"" d in - try - let dir = "mkdir -p " ^ d in - (match Unix.system dir with - | Unix.WEXITED 0 -> () - | Unix.WEXITED n -> - MatitaLog.error ("'mkdir -p " ^ dir ^ "' failed with "^string_of_int n); - failwith errmsg - | Unix.WSIGNALED s - | Unix.WSTOPPED s -> - MatitaLog.error - ("'mkdir -p " ^ dir ^ "' signaled with " ^ string_of_int s); - failwith errmsg) - with Unix.Unix_error _ as exc -> - MatitaLog.error - ("Unix error in makigin dir " ^ (MatitaExcPp.to_string exc)); - failwith errmsg -*) + let get_proof_status status = match status.proof_status with | Incomplete_proof s -> s