search

mozilla / galaxy

To infinity and beyond. The front-end UI.
BSD 3-Clause "New" or "Revised" License
10 stars 14 forks source link

Fixed build_directory script for non-bash users. #211

Closed adngdb closed 10 years ago

adngdb commented 10 years ago

pushd and popd are commands specific to bash. For people like me using other shells, the build_directory script can't work as is. This makes the script run under bash regardless of the user's shell.

@cvan r?

cvan commented 10 years ago

thanks! which shell are you using, out of curiosity? (I use zsh.)