Skip to content

Commit

Permalink
Rebuild test files when appropriate
Browse files Browse the repository at this point in the history
- Rebuild positive also upon new `agda2hs` binary
- Rebuild negative on new `agda2hs` binary, removing `force-recompile`
  • Loading branch information
naucke committed May 24, 2024
1 parent 7695157 commit 5926f94
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions test/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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' > $@

Expand Down

0 comments on commit 5926f94

Please sign in to comment.