diff options
| author | Novus Nota | 2023-12-17 21:40:29 +0000 |
|---|---|---|
| committer | GitHub | 2023-12-17 21:40:29 +0000 |
| commit | a1a20d231f509a01b7e0e8e040ce96206276ffd4 (patch) | |
| tree | f8d487212e6cba96aaa853fcb06f5011160c9035 /runtime/queries/agda | |
| parent | c56cd6ee8b9312a620d4fc38eea90a49613f5d72 (diff) | |
book: Describe usage of `.ignore` and helix-specific ignore files in `[editor.file-picker]` section (#9102)
Diffstat (limited to 'runtime/queries/agda')
0 files changed, 0 insertions, 0 deletions