src/Pure/ML-Systems/bash.ML
2010-02-07 ago modernized perl scripts: prefer standalone executables;
2010-02-06 ago renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;