| commit | 2d04b0da060037d2244c98776e5117fc9e6f8d53 | [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:19:55 2017 -0700 |
| tree | d413f1aa7d4f4cb74d955e4a70aad49d5d523dfe | |
| parent | 1b96a9571e6476efd841a8198635d6f673765870 [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