| Thu, 02 Jun 2016 17:05:40 +0200 | wenzelm | clarified aliases (no warning for duplicates); | changeset | files |
| Thu, 02 Jun 2016 16:49:44 +0200 | wenzelm | eliminated pointless alias (no warning for duplicates); | changeset | files |
| Thu, 02 Jun 2016 16:23:10 +0200 | wenzelm | avoid warnings on duplicate rules in the given list; | changeset | files |