On Mon, 2022-08-22 at 15:09 +0200, Marc Haber wrote: > I don't think so. People should still remove a comment sign and make > the > intended change.
Hmm I thought now people would consider this to refer to the "# Default: ..." line, which should stay as is. Anyway, thanks, Chris. :-)
