22 Oct
2022
22 Oct
'22
12:35 p.m.
On Sat Oct 22 06:40:16 2022 +0000, Chip Davis wrote:
I hate to be the bearer of bad news, since this was already merged, but it looks like you missed these two.
It's fixed by !1144. Thank you.