-
The pushd/popd commands are Bash-specific but in our simple case they can be easily replaced with plain cd, using `cd -' to switch back to the old dir. Also substitute the "&>/dev/null" redirection with ">/dev/null 2>&1". https://bugzilla.gnome.org/show_bug.cgi?id=700078
20afeb85