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

Temporarily making make verbose again.

Browse source
This commit is contained in:
Wen Kokke 2019-05-27 16:20:14 +01:00
parent a588fd4a9f
commit 0aa585b9b6
1 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
Makefile
View file

@ -30,15 +30,13 @@ out/:
# Build PLFA pages
out/%.md: src/%.lagda | out/
set -o pipefail && agda2html $(AGDA2HTML_FLAGS) -i $< -o $@ 2>&1 \
| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
agda2html $(AGDA2HTML_FLAGS) -i $< -o $@ 2>&1
@sed -i '1 s|---|---\nsrc : $(<)|' $@
# Build TSPL pages
out/%.md: tspl/%.lagda | out/
set -o pipefail; agda2html $(AGDA2HTML_FLAGS) -i $< -o $@ -- --include-path=$(realpath src) 2>&1 \
| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
agda2html $(AGDA2HTML_FLAGS) -i $< -o $@ -- --include-path=$(realpath src) 2>&1
@sed -i '1 s|---|---\nsrc : $(<)|' $@