From 54bd214a34224eab8c5ef2a26cb832c8b1ff122f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 3 Feb 2004 14:49:16 +0000 Subject: [PATCH] Check missed: the two metasenv were not compared. --- helm/gTopLevel/regtest.ml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml index 2530e34a0..8f42a29fc 100644 --- a/helm/gTopLevel/regtest.ml +++ b/helm/gTopLevel/regtest.ml @@ -108,6 +108,14 @@ let parse_regtest = let as_expected expected found = (* ignores "term" field *) let outcome = ref true in + if expected.emetasenv <> found.emetasenv then begin + print_msg "Metasenv mismatch"; + print_msg " expected:"; + print_msg (" " ^ expected.emetasenv); + print_msg " found:"; + print_msg (" " ^ found.emetasenv); + outcome := false; + end; if expected.eterm <> found.eterm then begin print_msg "Term mismatch"; print_msg " expected:"; -- 2.39.2