Mon, 07 Mar 2016 21:33:41 +0100 wenzelm tuned -- more standard operations;
Mon, 07 Mar 2016 21:09:28 +0100 wenzelm File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
Mon, 07 Mar 2016 20:44:47 +0100 wenzelm clarified treatment of DEL;
Mon, 07 Mar 2016 18:47:55 +0100 wenzelm clarified RAW_ML_SYSTEM;
Mon, 07 Mar 2016 18:31:40 +0100 wenzelm tuned;
Mon, 07 Mar 2016 18:20:22 +0100 wenzelm Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 tip