Thanks for your patience! It has been a long road with some dead ends (we've wanted to add this since 2012 at least). We actually wrote about why we didn't just use grep in our last blog post: https://github.blog/2023-02-06-the-technology-behind-githubs...