Sun, 21 Jan 2007 16:46:06 +0100 | wenzelm | *** MESSAGE REFERS TO PREVIOUS VERSION *** | changeset | files |
Sun, 21 Jan 2007 16:43:47 +0100 | wenzelm | tuned comments | changeset | files |
Sun, 21 Jan 2007 16:43:46 +0100 | wenzelm | simplified ML setup; | changeset | files |
Sun, 21 Jan 2007 16:43:45 +0100 | wenzelm | use_text: added name argument; | changeset | files |
Sun, 21 Jan 2007 16:43:44 +0100 | wenzelm | moved File.use to ML_Context.use; | changeset | files |
Sun, 21 Jan 2007 16:43:42 +0100 | wenzelm | use_text: added name argument; | changeset | files |