Sat, 18 May 2013 12:41:31 +0200 | wenzelm | explicit notion of public options, which are shown in the editor options dialog; | changeset | files |
Fri, 17 May 2013 23:31:02 +0200 | wenzelm | back to more paranoid interrupt test after request is cancelled -- avoid race condition; | changeset | files |