tree d413f1aa7d4f4cb74d955e4a70aad49d5d523dfe
parent 1b96a9571e6476efd841a8198635d6f673765870
author Zack Williams <zdw@cs.arizona.edu> 1506374395 -0700
committer Zack Williams <zdw@cs.arizona.edu> 1506374395 -0700

Use bash as the shell when building docs for pushd/popd

Change-Id: I4485959f0d451ea23a260d9c18bd6c79040c2e46