It should be the right place. Do you want to share the issue you opened so people can see it? By the way all the contributors are volunteers which means they spend free time on fixing issues, so you may not get responses. If it is urgent you should tag (mention) key contributors or submit pull request by yourself
@micuat Thanks for the response. No rush. Documentation fixes are rarely urgent .
I just wanted to make sure, that I hadn’t overlooked some other repository. Since there were no responses for issues and pull requests for this year, I was afraid I had found the wrong place.
Looking at Github Insights, I guess, @REAS or @shiffman are the ones responsible for the documentation? Since we are nearing the end of the semester, I understand, that people are busy.