| Thu, 07 Oct 1999 12:20:21 +0200 | wenzelm | tex_source: Buffer.write; | changeset | files |
| Thu, 07 Oct 1999 12:19:47 +0200 | wenzelm | present source *before* theory load; | changeset | files |
| Thu, 07 Oct 1999 12:19:21 +0200 | wenzelm | removed write_nonempty; | changeset | files |
| Thu, 07 Oct 1999 11:39:47 +0200 | berghofe | New option -d for deleting file after use. | changeset | files |