diff options
| author | Ben Lee-Cohen | 2022-05-05 15:58:18 +0000 |
|---|---|---|
| committer | GitHub | 2022-05-05 15:58:18 +0000 |
| commit | 2f240b018eb95457441a0cad9b7af47b0e55a54c (patch) | |
| tree | dada2811adf7a81701a00756421a6acf9a70f23b /runtime/queries/lean/highlights.scm | |
| parent | a5f4925f53d447bb7201c9a6e7a1c2730f292ae4 (diff) | |
Adding the global gitignore to the default (#2410)
Diffstat (limited to 'runtime/queries/lean/highlights.scm')
0 files changed, 0 insertions, 0 deletions