From: Claudio Sacerdoti Coen Date: Tue, 3 Feb 2004 14:40:14 +0000 (+0000) Subject: Debuggin infos removed. X-Git-Tag: V_0_2_3~89 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=646303b5ddd2daf3ca5f0e34e830d43057e866bd;p=helm.git Debuggin infos removed. --- diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml index 73eaf06ee..2530e34a0 100644 --- a/helm/gTopLevel/regtest.ml +++ b/helm/gTopLevel/regtest.ml @@ -100,7 +100,6 @@ let parse_regtest = | l -> Buffer.add_string (buffer_of_state !state) (line ^ "\n") done with End_of_file -> ()); -prerr_endline ("@@@ " ^ Buffer.contents emetasenv); { term = Buffer.contents term; emetasenv = Buffer.contents emetasenv; eterm = Buffer.contents eterm;