17 Nov
2023
17 Nov
'23
12:08 p.m.
On Fri Nov 17 12:08:39 2023 +0000, Conor McCarthy wrote:
The condition on the following lines handled this, but I've simplified it.
I'm still not convinced, but I commented on the new code.