On Thu, Jul 09, 2020 at 10:21:57PM -0400, Andrew Dunstan wrote:
> I certainly agree we should document more clearly why it's there, to
> help forestall anyone else who comes along and thinks it would just be
> neater to remove it. so +1.
Okay. Done, then.
--
Michael