Bashisms pushd/popd don't work so well if /bin/sh is dash, as is the case on a Debian machine.