From d1163c6f391364dd693826d5304d98bd7afc76ee Mon Sep 17 00:00:00 2001 From: Pepijn Kokke Date: Tue, 14 Mar 2017 16:13:06 +0000 Subject: [PATCH] Removed --strip-implicits. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index fa0a5d17..0709a40c 100644 --- a/Makefile +++ b/Makefile @@ -8,7 +8,7 @@ out/: mkdir out out/%.md: src/%.lagda out/ - agda2html --strip-implicit-args --link-to-agda-stdlib --link-local -i $< -o $@ + agda2html --link-to-agda-stdlib --link-local -i $< -o $@ .phony: clean