| Mon, 02 Nov 2015 18:31:57 +0100 | wenzelm | avoid premature flushing and thus flashing of text area; | changeset | files |
| Mon, 02 Nov 2015 18:30:25 +0100 | wenzelm | tuned whitespace; | changeset | files |
| Mon, 02 Nov 2015 18:09:14 +0100 | wenzelm | clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a); | changeset | files |