diff options
| author | Blaž Hrastnik | 2022-02-13 09:31:51 +0000 |
|---|---|---|
| committer | Blaž Hrastnik | 2022-02-13 09:31:51 +0000 |
| commit | bd549d8a20cce98e24c8653a4a86107c786cbaa3 (patch) | |
| tree | 0780b58d41b6181e69023265cdb54517e2953778 /runtime/queries/lean/locals.scm | |
| parent | 7ad8eaaef0b292f4be6c66298cea40d2b928e172 (diff) | |
| parent | 7083b98a388b30e0b61caac9bf6ccc1d79eadf81 (diff) | |
Merge remote-tracking branch 'origin/master' into debug
Diffstat (limited to 'runtime/queries/lean/locals.scm')
| -rw-r--r-- | runtime/queries/lean/locals.scm | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/runtime/queries/lean/locals.scm b/runtime/queries/lean/locals.scm new file mode 100644 index 00000000..dd6c2036 --- /dev/null +++ b/runtime/queries/lean/locals.scm @@ -0,0 +1,5 @@ +[ + (module) + (namespace) + (section) +] @local.scope |