Wed, 27 Aug 2008 20:36:27 +0200 | wenzelm | renamed Buffer.write to File.write_buffer; | changeset | files |
Wed, 27 Aug 2008 20:36:26 +0200 | wenzelm | renamed Buffer.write to File.write_buffer; | changeset | files |
Wed, 27 Aug 2008 20:36:25 +0200 | wenzelm | load buffer.ML before file.ML; | changeset | files |
Wed, 27 Aug 2008 20:36:23 +0200 | wenzelm | replaced find_substring by first_field; | changeset | files |