Removed --strip-implicits.
This commit is contained in:
parent
a3f809994d
commit
d1163c6f39
1 changed files with 1 additions and 1 deletions
2
Makefile
2
Makefile
|
@ -8,7 +8,7 @@ out/:
|
||||||
mkdir out
|
mkdir out
|
||||||
|
|
||||||
out/%.md: src/%.lagda 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
|
.phony: clean
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue