diff options
| author | Jonathan LEI | 2022-10-19 00:53:58 +0000 |
|---|---|---|
| committer | GitHub | 2022-10-19 00:53:58 +0000 |
| commit | 1a772d1b67d4895d79273b027b1b1f86bd1616fe (patch) | |
| tree | e8e6229f1b7ecf37a4b1cc73d260d707bdf52c69 /runtime/queries/lean/highlights.scm | |
| parent | 0c14d9f869c503a873a420c4acab17bd922d1d3b (diff) | |
Fix deleting word from end of buffer (#4328)
Diffstat (limited to 'runtime/queries/lean/highlights.scm')
0 files changed, 0 insertions, 0 deletions