diff options
| author | Blaž Hrastnik | 2021-12-06 03:48:25 +0000 |
|---|---|---|
| committer | Blaž Hrastnik | 2021-12-06 03:48:25 +0000 |
| commit | a2b22ec15207926acf9bbf6617492925a6e50d27 (patch) | |
| tree | 3026c4e0f92433510db13ba86eefa13d83568198 /.github | |
| parent | cab09093dd5bf9b4707bfdfd8529b348c02670ea (diff) | |
Use binary_search when looking up diagnostics
They're sorted by range so they should also be sorted by line
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions