15 Feb
2022
15 Feb
'22
10:32 p.m.
I'd do the oneliner changing it to 5 and be done with it. That being said, we have plenty of examples of doing this both ways, so whatever makes people happy.
Excellent, that's the patch I wrote originally :-)
Dropping this patch, unless Angelo (or someone else) strongly objects.