indexing projects that are not the root of the repository

[kim-em]

Cedar is a great example of a project where the Lean project is in a subdirectory of the main git repository, but we really ought to have on Reservoir!

[tydeu]

Right now, I do not see an feasible way to do this. There are two major problems:

1. GitHub code search already has a very low limit on search results (and thus using it already is not heavily scalable). Extending the search to any file in a repository would quickly shoot past the limits.
2. Repositories can easily have multiple lakefiles. Many of these "pacakges" are things we definitely do not want in Reservoir (e.g., examples). It is thus not clear how to perform such a search without picking up a lot of bad results.

[kim-em]

User registration!