Thanks Sebastian We are now since a couple of years managing Pharo via github. I can do a Pull Request with you changes. Now it may be a good occasion for you to practice. Let me know if you want to try by yourself.
https://github.com/pharo-project/pharo/wiki/Contribute-a-fix-to-Pharo <https://github.com/pharo-project/pharo/wiki/Contribute-a-fix-to-Pharo> S.
