From 9752444a812eb8970bc4105a3970f557d7ce7c5c Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 6 Jun 2023 11:31:42 +1000 Subject: [PATCH] run_tests: REFINE_QUICK_AND_DIRTY already set in Makefile REFINE_QUICK_AND_DIRTY is already set correctly in proofs/Makefile, so doesn't need to be set here. Signed-off-by: Gerwin Klein --- run_tests | 5 ----- 1 file changed, 5 deletions(-) diff --git a/run_tests b/run_tests index f5d087ff6..8704a934d 100755 --- a/run_tests +++ b/run_tests @@ -133,11 +133,6 @@ for arch in archs: elif "L4V_ARCH_IS_ARM" in os.environ: del os.environ["L4V_ARCH_IS_ARM"] - # Permit sorries in AARCH64 Refine during development - if arch == "AARCH64": - os.environ["REFINE_QUICK_AND_DIRTY"]="1" - print("Testing AARCH64 Refine in quick and dirty mode") - sys.stdout.flush() # Arguments: