6 Apr
2023
6 Apr
'23
12:14 p.m.
On Thu Apr 6 11:25:59 2023 +0000, Giovanni Mascellani wrote:
Minor, but we put only one rule name per `%type` directive.
There is another instance when there are several, but I don't see how this is important.