On Thu, May 12, 2022 at 8:44 AM Bart Schaefer <schaefer@brasslantern.com> wrote:
>
> What's the .vscode/settings.json file in the patch?

Oh, whoops, that shouldn't be there. Here's a new version of the patch.