diff options
| author | Ravi Shekhar Jethani | 2023-07-23 07:45:13 +0000 |
|---|---|---|
| committer | GitHub | 2023-07-23 07:45:13 +0000 |
| commit | 48d57dad471a0cb8b26aa93edc379f38b813ad72 (patch) | |
| tree | 9d0163882a646b772ece690365c0df1d09da384e /book/src | |
| parent | 505213d41b5a4807431f623fae53180e06d867a7 (diff) | |
Fix selection highlighting in remaining gruvbox derived themes (#7717)
Diffstat (limited to 'book/src')
0 files changed, 0 insertions, 0 deletions