Closed chalmerlowe closed 7 hours ago
🤖 I detect that the PR title and the commit message differ and there's only one commit. To use the PR title for the commit history, you can use Github's automerge feature with squashing, or use automerge
label. Good luck human!
-- conventional-commit-lint bot https://conventionalcommits.org/
This corrects several minor errors in type annotations.