diff options
| author | Frojdholm | 2022-06-02 07:54:11 +0000 |
|---|---|---|
| committer | GitHub | 2022-06-02 07:54:11 +0000 |
| commit | f7c27b604f32cbd10ec42f70d3fec3ff79cacc63 (patch) | |
| tree | fea1ea37df278bf1a60502c31456e38b848400b7 /runtime/queries/lean/injections.scm | |
| parent | 378f438fb033561831cd6e0f94845feaf82bbbcb (diff) | |
Ignore SendErrors when handling grammars (#2641)
When handling grammars, fetching and building is done in a thread
pool. Results are communicated over channels and the receiving
channel is closed on first error. This causes subsequent sends to
fail causing a mess in stderr. This ignores all SendErrors causing
only the first error to be printed.
Diffstat (limited to 'runtime/queries/lean/injections.scm')
0 files changed, 0 insertions, 0 deletions