diff --git a/docs/Makefile b/docs/Makefile
index b725a42..df03d5b 100644
--- a/docs/Makefile
+++ b/docs/Makefile
@@ -1,5 +1,8 @@
 default: serve
 
+# use bash for pushd/popd, and to fail if commands within  a pipe fail
+SHELL = bash -o pipefail
+
 GENERATED_DOCS = build_glossary.md
 
 serve: setup