From 0d0d9c6b89ec77859b4b278f694e572e28b096c0 Mon Sep 17 00:00:00 2001
From: Yuri Astrakhan <yuriastrakhan@gmail.com>
Date: Mon, 4 May 2020 16:41:55 -0400
Subject: [PATCH] Don't hide makefile errors in pipes (#848)

Follow up to #846 - make sure that if an error happens inside a target whose output is piped, we stop.
---
 Makefile | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Makefile b/Makefile
index a1da367..47f0746 100644
--- a/Makefile
+++ b/Makefile
@@ -1,3 +1,7 @@
+# Ensure that errors don't hide inside pipes
+SHELL         = /bin/bash
+.SHELLFLAGS   = -o pipefail -c
+
 # Options to run with docker and docker-compose - ensure the container is destroyed on exit
 # Containers run as the current user rather than root (so that created files are not root-owned)
 DC_OPTS?=--rm -u $(shell id -u):$(shell id -g)