> IMO, leave it to the person willing to make the PR, it can always be moved > later if it turns out people are using it a lot for some reason or having > trouble finding it.
Sure, but if we don't ask we don't know if the OP is happy to do it. -- You are receiving this because you are subscribed to this thread. Reply to this email directly or view it on GitHub: https://github.com/geany/geany/pull/2695#issuecomment-748719248