tree e0f71324602c1d3e554c371030cadcaadda95f6e
parent 6e87cbc4ceb9c1b2d63b30eb5465176290be03f3
author Zack Williams <zdw@cs.arizona.edu> 1506374395 -0700
committer Zack Williams <zdw@cs.arizona.edu> 1506374431 -0700

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

Change-Id: I4485959f0d451ea23a260d9c18bd6c79040c2e46