| Mon, 28 Dec 2015 19:23:15 +0100 | wenzelm | more symbols; | changeset | files |
| Mon, 28 Dec 2015 18:03:26 +0100 | wenzelm | use symbols by default; | changeset | files |
| Mon, 28 Dec 2015 17:43:30 +0100 | wenzelm | prefer symbols for "Union", "Inter"; | changeset | files |
| Mon, 28 Dec 2015 16:34:26 +0100 | wenzelm | clarified position information; | changeset | files |
| Mon, 28 Dec 2015 16:30:24 +0100 | wenzelm | suppress irrelevant position reports; | changeset | files |
| Mon, 28 Dec 2015 16:29:39 +0100 | wenzelm | suppress irrelevant position reports; | changeset | files |
| Mon, 28 Dec 2015 16:13:15 +0100 | wenzelm | tuned; | changeset | files |