diff options
| author | Mark Stosberg | 2024-02-12 16:48:10 +0000 |
|---|---|---|
| committer | GitHub | 2024-02-12 16:48:10 +0000 |
| commit | 0516337abb7096c7d909624a7e1307ee4b837835 (patch) | |
| tree | ec47291955ed3475fd7678f69f7b65380a75adb6 /runtime/queries/agda | |
| parent | bb1e2ddcd8c01256d81ae712090c4ca1e2d09561 (diff) | |
docs: Document that what the `diff` gutter symbol does (#9587)
Before there was no document about what the `diff` gutter is displaying
or what the colors mean.
These docs clarify it's a `git` diff and makes it easier to
cross-reference the theme if you aren't sure what the colors mean or
want to change them.
Diffstat (limited to 'runtime/queries/agda')
0 files changed, 0 insertions, 0 deletions