michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Removed agda2html from the Makefile

Browse source
This commit is contained in:
Wen Kokke 2019-07-12 15:05:43 +01:00
parent 1867023b20
commit 2ebe3264a0
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
Makefile
View file

@ -109,7 +109,6 @@ macos-setup:
# Travis Setup (install Agda, the Agda standard library, agda2html, acknowledgements, etc.)
travis-setup:\
$(HOME)/.local/bin/agda\
$(HOME)/.local/bin/agda2html\
$(HOME)/.local/bin/acknowledgements\
$(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src\
$(HOME)/.agda/defaults\