On Fri, Dec 23, 2022 at 08:16:58PM -0700, Tycho Andersen wrote: > Otherwise it's hard to tell where this came from, and we qualify most > everything else in this file anyway. Ping, just ran across this again. Should I make a PR instead? Thanks. Tycho