search

breck7 / pldb

PLDB: a Programming Language DataBase
https://pldb.io
732 stars 99 forks source link

Drop "githubRepo" data key in favor of one named e.g. "sourceRepo" #521

Closed ell1e closed 11 months ago

ell1e commented 11 months ago

edit: misguided request

breck7 commented 11 months ago

Hi @ell1e the key gitRepo is for cases where the primary repo is self-hosted. So the official main repo should always be listed even if it's self-hosted. There is also githubRepo, gitlabRepo, et cetera.

Having a separate key for source hosting service provided more context for the crawl scripts and autocomplete (having stars as a subkey for githubRepo makes sense but not under gitRepo). I think at one point I tried using a 2 part key with part 1 being gitRepo and part 2 being the domain name of the provided URL, but that required more work on the tooling end.