>>> Sollte »mini« nicht auch als Präfix behandelt werden?
>>
>> [...] Andererseits ist der Präfixcharakter nicht von der Hand zu
>>weisen; ich hätte also nichts gegen eine Änderung.
>
> Gern. Das war halt schon so, bevor wir die Präfixe markiert haben.
Ist jetzt erledigt.
Werner