src/Pure/ML-Systems/bash.ML
Sun, 07 Feb 2010 20:21:38 +0100 wenzelm modernized perl scripts: prefer standalone executables;
Sat, 06 Feb 2010 14:50:55 +0100 wenzelm renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
less more (0) tip