github's code search is notoriously bad, feels like a huge missed opportunity. Nice to see you guys reaching out to other people working in this area.
Then i had to download repo in my local; run VS code (updating first), search there, modify, push. I wish i could do this on Ghub web GUI
TIL some of them are on this page that you only see if you search for an empty string:
Click on 'prefixes'. This kind of thing should be readily available from any search box that searches through GitHub.
I think there were better solutions on the early 2000’s.