Closed tleedjarv closed 1 year ago
Closes #862
Github needs a new badge for "filed a PR to fix a new issue within 15 minutes of the issue, and PR was merged before CI finished"!!
Closes #862