From 2ebe3264a0182838e35823d75c286aabe90aa256 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Fri, 12 Jul 2019 15:05:43 +0100 Subject: [PATCH] Removed agda2html from the Makefile --- Makefile | 1 - 1 file changed, 1 deletion(-) diff --git a/Makefile b/Makefile index 32e8bee1..9326d0f7 100644 --- a/Makefile +++ b/Makefile @@ -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\