| Mon, 20 Aug 2007 20:44:01 +0200 | wenzelm | tuned signature; | changeset | files |
| Mon, 20 Aug 2007 20:44:00 +0200 | wenzelm | File.read/write/append: non-critical (basic IO operations already thread-safe); | changeset | files |
| Mon, 20 Aug 2007 20:43:59 +0200 | wenzelm | TextIO.inputLine: non-critical (assume exclusive ownership); | changeset | files |