diff options
| author | Michael Davis | 2022-02-19 10:51:14 +0000 |
|---|---|---|
| committer | Blaž Hrastnik | 2022-03-10 08:31:57 +0000 |
| commit | 6fcab90d16f9493c0c4738312061a26e473ab12a (patch) | |
| tree | b06f59ecb48f5ba6e518ec79438b8c82bfba903c /.github | |
| parent | a229f405cc0d9690fc9ceca99fce0832b3e060ab (diff) | |
only fetch git-sourced grammars
This is a bit of a micro-optimization: in the current setup we waste
a thread in the pool for a local grammar only to println! a message
saying we're skipping fetching because it's a local grammar.
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions