Skip to content

Commit 8318806

Browse files
committed
[ ci ] whyyyyy?!
1 parent 74114fb commit 8318806

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

tests/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ AGDA_BUILD_DIR = _config/_build
77
CABAL_BUILD_DIR = _config/dist-newstyle
88

99
./runtests: admin/runtests/runtests.agda
10-
cd admin/runtests && sh run
10+
cd admin/runtests && AGDA="$(AGDA)" sh run
1111

1212
test: ./runtests
1313
./runtests "$(AGDA)" $(INTERACTIVE) --timing --failure-file failures --only $(only)

0 commit comments

Comments
 (0)