Hi, Paul Gevers <[email protected]> wrote (Sun, 15 Jun 2025 13:50:58 +0200): > Hi, > > On 15-06-2025 13:25, Holger Wansing wrote: > > So, do we want this change? > > > I think so.
Ok, just pushed to git. -- Holger Wansing <[email protected]> PGP-Fingerprint: 496A C6E8 1442 4B34 8508 3529 59F1 87CA 156E B076

