p.s. is this the correct way to report this or can I create a PR someplace?
Ofcourse there is no harm in reporting it here, but I think most developers are more active on the corresponding github pages. See:
To quickly find the github repository you can click the litle arrow on the top right of the tool.