Removed --local-references flag
This commit is contained in:
parent
02fc506bd0
commit
060e411323
1 changed files with 1 additions and 1 deletions
2
Makefile
2
Makefile
|
@ -14,7 +14,7 @@ out/:
|
||||||
mkdir -p out/
|
mkdir -p out/
|
||||||
|
|
||||||
out/%.md: src/%.lagda | out/
|
out/%.md: src/%.lagda | out/
|
||||||
agda2html --verbose --link-to-agda-stdlib --link-to-local-agda-names --local-references --use-jekyll=out/ -i $< -o $@ 2>&1 \
|
agda2html --verbose --link-to-agda-stdlib --link-to-local-agda-names --use-jekyll=out/ -i $< -o $@ 2>&1 \
|
||||||
| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
|
| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
|
||||||
@sed -i '1 s|---|---\nsrc : $(<)|' $@
|
@sed -i '1 s|---|---\nsrc : $(<)|' $@
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue