src/Pure/System/command_line.ML
Wed, 08 Aug 2012 12:33:40 +0200 wenzelm more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
Sun, 05 Aug 2012 13:42:21 +0200 wenzelm prefer general Command_Line.tool wrapper (cf. Scala version);
less more (0) tip