Tue, 22 Dec 2015 14:31:39 +0100 | wenzelm | merged | changeset | files |
Tue, 22 Dec 2015 14:26:35 +0100 | wenzelm | more thorough event propagation; | changeset | files |
Tue, 22 Dec 2015 14:23:39 +0100 | wenzelm | tuned -- with subtle change of order of evaluation; | changeset | files |