From 5926f943c16de615ef7c14547ee1a89da0c87e8d Mon Sep 17 00:00:00 2001 From: Jakob Naucke Date: Thu, 23 May 2024 19:32:02 +0200 Subject: [PATCH] Rebuild test files when appropriate - Rebuild positive also upon new `agda2hs` binary - Rebuild negative on new `agda2hs` binary, removing `force-recompile` --- test/Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/Makefile b/test/Makefile index d3868cd8..ed87e47a 100644 --- a/test/Makefile +++ b/test/Makefile @@ -8,7 +8,7 @@ FAIL_MAIN=AllFailTests default : compare -build/%.hs : %.agda *.agda Fail/*.agda Cubical/*.agda +build/%.hs : %.agda *.agda Fail/*.agda Cubical/*.agda agda2hs @echo == Compiling tests == $(AGDA2HS) $< -o build @@ -21,7 +21,7 @@ print-fail : fail : print-fail $(patsubst Fail/%.agda,build/%.err,$(wildcard Fail/*.agda)) -build/%.err : Fail/%.agda force-recompile +build/%.err : Fail/%.agda agda2hs @echo Compiling $< @($(AGDA2HS) $< -o build -v0 && echo "UNEXPECTED SUCCESS" || true) | sed -e 's:'$(ROOT)'::g' > $@