24 Aug
2022
24 Aug
'22
12:14 a.m.
On Wed Aug 24 00:14:19 2022 +0000, Davide Beatrici wrote:
Just realized I didn't append a period to the commit messages. I'll fix that right after !687 (or another MR) is merged, in order to avoid triggering an unnecessary CI pipeline.
Done.