| commit | 7f68d0a2f287643a111ad7f7e179cf67fa3c99db | [log] [tgz] |
|---|---|---|
| author | Zack Williams <zdw@cs.arizona.edu> | Mon Sep 25 14:19:55 2017 -0700 |
| committer | Zack Williams <zdw@cs.arizona.edu> | Mon Sep 25 14:20:31 2017 -0700 |
| tree | e0f71324602c1d3e554c371030cadcaadda95f6e | |
| parent | 6e87cbc4ceb9c1b2d63b30eb5465176290be03f3 [diff] [blame] |
Use bash as the shell when building docs for pushd/popd Change-Id: I4485959f0d451ea23a260d9c18bd6c79040c2e46
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