21 Dec
2022
21 Dec
'22
7:19 a.m.
Hi, Am Freitag, dem 09.12.2022 um 19:31 +0100 schrieb Joachim Breitner:
Am Dienstag, dem 29.11.2022 um 17:14 +0100 schrieb Joachim Breitner:
Happy to hear more voices and accept with whatever the majority of voices said they’d prefer (without formal votes, doesn’t seem to be worth it), assuming nobody thinks either way is a showstopper.
didn’t hear more on this issue. If silence continues for a few more days, I’ll accept it (in the current variant ({-# WARNING [x-partial] #-}), by popular vote).
accepted and merged! Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/