27 Nov
2023
27 Nov
'23
11:03 a.m.
On Mon Nov 27 11:00:09 2023 +0000, Matteo Bruni wrote:
Good catch, I'll send that fix in a followup (unless Paul wants to take care of it as well).
Actually Paul did this in the final (now merged) version of this MR, so we're good.