[ admin ] allow caller to pick agda executable

gallais · May 12, 2023 · 6772e02 · 6772e02
1 parent d904bd2
commit 6772e02
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/Makefile b/Makefile
@@ -1,14 +1,15 @@
+AGDA_EXEC?=agda
 .PHONY: test Everything.agda clean
 
 OTHEROPTS = --auto-inline -Werror
 
 RTSARGS = +RTS -M6G -A128M -RTS ${OTHEROPTS}
 
 test: Everything.agda
-	agda ${RTSARGS} -i. Everything.agda
+	${AGDA_EXEC} ${RTSARGS} -i. Everything.agda
 
 html: Everything.agda
-	agda ${RTSARGS} --html -i. Everything.agda
+	${AGDA_EXEC} ${RTSARGS} --html -i. Everything.agda
 
 Everything.agda:
 	git ls-tree --full-tree -r --name-only HEAD | grep '^src/[^\.]*.agda' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' | LC_COLLATE='C' sort > Everything.agda