Thu, 11 Nov 2010 16:48:46 +0100 | wenzelm | replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes; | changeset | files |
Thu, 11 Nov 2010 13:23:39 +0100 | wenzelm | tuned; | changeset | files |
Thu, 11 Nov 2010 13:07:41 +0100 | wenzelm | reduced danger of line breaks within minipage; | changeset | files |