From 646303b5ddd2daf3ca5f0e34e830d43057e866bd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 3 Feb 2004 14:40:14 +0000 Subject: [PATCH] Debuggin infos removed. --- helm/gTopLevel/regtest.ml | 1 - 1 file changed, 1 deletion(-) 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; -- 2.39.2