adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

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 <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-06-06 11:31:42 +10:00 committed by Gerwin Klein
parent 290b7c73cc
commit 9752444a81
1 changed files with 0 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
run_tests
View File

@ -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: