Sat, 17 Aug 2013 22:58:48 +0200 | wenzelm | Sledgehammer is docked on startup; | changeset | files |
Sat, 17 Aug 2013 22:45:48 +0200 | wenzelm | prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options; | changeset | files |
Sat, 17 Aug 2013 22:27:41 +0200 | wenzelm | more robust startup; | changeset | files |