X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMisc.ml;h=df124751f1fe6e21480fb45a133ecaa0e2c8a79f;hb=refs%2Fheads%2Fmaster;hp=53d1d1f67ec2440c2c3ce45df0958ab52b9edfd3;hpb=3df31c02806eca83c63c14e6a89844f764c3e2cb;p=helm.git diff --git a/matita/matita/matitaMisc.ml b/matita/matita/matitaMisc.ml index 53d1d1f67..df124751f 100644 --- a/matita/matita/matitaMisc.ml +++ b/matita/matita/matitaMisc.ml @@ -38,8 +38,8 @@ let strip_suffix ~suffix s = let absolute_path file = if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file -let is_proof_script _fname = true (** TODO Zack *) -let is_proof_object _fname = true (** TODO Zack *) +let is_proof_script _fname = true (* TODO Zack *) +let is_proof_object _fname = true (* TODO Zack *) let append_phrase_sep s = if not (Pcre.pmatch ~pat:(sprintf "%s$" BuildTimeConf.phrase_sep) s) then @@ -154,13 +154,6 @@ let list_tl_at ?(equality=(==)) e l = 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) -*) - (* FG: out_preamble *********************************************************) let out_comment och s =