Thu, 10 Nov 2016 10:41:41 +0100 | wenzelm | proper cleanup; | changeset | files |
Thu, 10 Nov 2016 10:35:34 +0100 | wenzelm | uniform order for options and args; | changeset | files |
Thu, 10 Nov 2016 10:20:11 +0100 | wenzelm | more robust jedit_auto_resolve: avoid losing events deps_changed() / delay_load.invoke(); | changeset | files |