diff options
| author | Christoph Horn | 2022-08-24 08:32:08 +0000 |
|---|---|---|
| committer | Michael Davis | 2022-08-24 16:55:47 +0000 |
| commit | 26b2f0a1b5a1bb6cd83f16f6019d903312999bb9 (patch) | |
| tree | e0a6ca3d54c9d563a404d82626e8138e1f5ab130 /runtime/queries/lean | |
| parent | 5806db1e5cd52897bf0cda4421629eec207a621c (diff) | |
Julia queries: prevent constructors to be highlighted as functions
Also improves the captures of the remaining identifiers.
Diffstat (limited to 'runtime/queries/lean')
0 files changed, 0 insertions, 0 deletions