| Wed, 15 Jun 2011 16:26:09 +0200 | wenzelm | more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension); | changeset | files |
| Wed, 15 Jun 2011 16:22:58 +0200 | wenzelm | more robust init; | changeset | files |
| Wed, 15 Jun 2011 15:42:54 +0200 | wenzelm | recovered orig_text_painter from f4141da52e92; | changeset | files |
| Wed, 15 Jun 2011 15:08:22 +0200 | wenzelm | tuned; | changeset | files |