From: Andrea Asperti Date: Fri, 22 Jul 2005 13:54:08 +0000 (+0000) Subject: Removed debugging print. X-Git-Tag: V_0_7_2~105 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=afde811cd8ac8fdfebf169dfb1196493e42bbba1;p=helm.git Removed debugging print. --- diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml index d95bfdbad..48d669628 100644 --- a/helm/matita/matitamakeLib.ml +++ b/helm/matita/matitamakeLib.ml @@ -213,7 +213,6 @@ let mk_maker refresh_cb = try let argv = Array.of_list ("make"::args) in pid := Unix.create_process "make" argv Unix.stdin out_w err_w; -let ch = open_out "/tmp/pippo" in output_string ch (String.concat " " ("make"::(Array.to_list argv)) ^ "\n"); flush ch; close_out ch; Unix.close out_w; Unix.close err_w; let buf = String.create 1024 in