On 6/23/22 14:32, Eliot Miranda wrote:
>>> ... should it be removed?
> 
> Is it that big a deal?  If so, certainly.  If not, IIABDFI

("If it's a big deal, forget it?")

No, it's not very important. I just noticed it was there and went 
"what's *that*??" :-)

It feels like something that'd be nice to clean up, but if it stays it's 
doing no material harm.