aboutsummaryrefslogtreecommitdiff
path: root/runtime/queries/lean/highlights.scm
diff options
context:
space:
mode:
authorJonathan LEI2022-10-19 00:53:58 +0000
committerGitHub2022-10-19 00:53:58 +0000
commit1a772d1b67d4895d79273b027b1b1f86bd1616fe (patch)
treee8e6229f1b7ecf37a4b1cc73d260d707bdf52c69 /runtime/queries/lean/highlights.scm
parent0c14d9f869c503a873a420c4acab17bd922d1d3b (diff)
Fix deleting word from end of buffer (#4328)
Diffstat (limited to 'runtime/queries/lean/highlights.scm')
0 files changed, 0 insertions, 0 deletions