From d2d3a86dad81170eeba278bbcf3839e70a0611ee Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Mon, 27 May 2019 14:54:30 +0100
Subject: [PATCH] Added 'set -o pipefail' to Makefile

---
 Makefile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Makefile b/Makefile
index 753ddf8a..c628103d 100644
--- a/Makefile
+++ b/Makefile
@@ -30,14 +30,14 @@ out/:
 
 # Build PLFA pages
 out/%.md: src/%.lagda | out/
-	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 -i '1 s|---|---\nsrc       : $(<)|' $@
 
 
 # Build TSPL pages
 out/%.md: tspl/%.lagda | out/
-	agda2html $(AGDA2HTML_FLAGS) -i $< -o $@ -- --include-path=$(realpath src) 2>&1 \
+	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'
 	@sed -i '1 s|---|---\nsrc       : $(<)|' $@