22 Oct
2025
22 Oct
'25
5:55 p.m.
On Wed Oct 22 16:51:12 2025 +0000, Gabriel Ivăncescu wrote:
Ah right. Should I add it as a separate commit, regardless? It would still be useful later on.
It's not used by this MR, so no. It can be added when it will be used.