Hi @MichaelMure, I've prepared a fix for this issue, but I can't push since do not have correct access rights 👀
Is there anything on my side that should be fixed?
Michael Muré (MichaelMure) commented
The normal github process it to:
make a fork on your own account
add that repo as a git remote
push there
create a pull-request (you get an easy link for that when you push the first time)
Serhii Vasylkov (vasser) commented
Thank you for explanation. I can open a PR with contribution file as a separate PR if you do not mind