Fixed Makfile and set Travis shell to BASH
This commit is contained in:
parent
d2d3a86dad
commit
aa32fad7d8
2 changed files with 5 additions and 1 deletions
|
@ -24,6 +24,10 @@ addons:
|
||||||
- libgmp-dev
|
- libgmp-dev
|
||||||
- libicu-dev
|
- libicu-dev
|
||||||
|
|
||||||
|
# Ensure we run BASH and not SH
|
||||||
|
env:
|
||||||
|
- SH=bash
|
||||||
|
|
||||||
before_install:
|
before_install:
|
||||||
# Download and unpack the stack executable
|
# Download and unpack the stack executable
|
||||||
- mkdir -p ~/.local/bin
|
- mkdir -p ~/.local/bin
|
||||||
|
|
2
Makefile
2
Makefile
|
@ -30,7 +30,7 @@ out/:
|
||||||
|
|
||||||
# Build PLFA pages
|
# Build PLFA pages
|
||||||
out/%.md: src/%.lagda | out/
|
out/%.md: src/%.lagda | out/
|
||||||
set -o pipefail; agda2html $(AGDA2HTML_FLAGS) -i $< -o $@ 2>&1 \
|
set -o pipefail && agda2html $(AGDA2HTML_FLAGS) -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