Unnamed repository; edit this file 'description' to name the repository.
Diffstat (limited to 'runtime/queries/lean/locals.scm')
| -rw-r--r-- | runtime/queries/lean/locals.scm | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/runtime/queries/lean/locals.scm b/runtime/queries/lean/locals.scm deleted file mode 100644 index dd6c2036..00000000 --- a/runtime/queries/lean/locals.scm +++ /dev/null @@ -1,5 +0,0 @@ -[ - (module) - (namespace) - (section) -] @local.scope |