File tree Expand file tree Collapse file tree 1 file changed +8
-7
lines changed
Expand file tree Collapse file tree 1 file changed +8
-7
lines changed Original file line number Diff line number Diff line change 1- .PHONY : test Everything.agda clean
1+ .PHONY : test html Everything.agda clean profile
22
3- OTHEROPTS = --auto-inline -Werror
4-
5- RTSARGS = +RTS -M6G -A128M -RTS ${OTHEROPTS}
3+ AGDA_EXEC = agda
4+ OTHEROPTS = -Werror
5+ RTSARGS = +RTS -M6G -A128M -RTS
6+ AGDA =$(AGDA_EXEC ) $(OTHEROPTS ) $(RTSARGS )
67
78test : Everything.agda
8- agda ${RTSARGS} -i. Everything.agda
9+ $( AGDA ) -i. Everything.agda
910
1011html : Everything.agda
11- agda ${RTSARGS} --html -i. Everything.agda
12+ $( AGDA ) --html -i. Everything.agda
1213
1314Everything.agda :
1415 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
1718 find . -name ' *.agdai' -exec rm \{\} \;
1819
1920profile : Everything.agda
20- agda ${RTSARGS} -v profile:7 -v profile.definitions:15 -i. Everything.agda
21+ $( AGDA ) -v profile:7 -v profile.definitions:15 -i. Everything.agda
You can’t perform that action at this time.
0 commit comments