On Friday, 12 June 2026 at 22:35:31 UTC, ABRightLight wrote: >> I would have posted this to `digitalmars.dip.ideas`. > > I didn't think a small change like this would need to be a DIP. > Should I double-post? If it gains no traction in here, why not?