diff options
| author | ChrHorn | 2022-10-03 14:44:45 +0000 |
|---|---|---|
| committer | GitHub | 2022-10-03 14:44:45 +0000 |
| commit | 589d17c7583716b339875b72972aaffe0ae5efc1 (patch) | |
| tree | 4351301a2de7cc146cdb041e31ff643982d4e4a4 /runtime/themes | |
| parent | 6939dd3adb4ccd89ce63e69d9b0586a377a4df42 (diff) | |
Add `ui.gutter.selected` option for themes (#3303)
* add `ui.gutter.selected`
* add `ui.gutter`, `ui.gutter.selected` to docs
Diffstat (limited to 'runtime/themes')
0 files changed, 0 insertions, 0 deletions