ChrHorn 589d17c758 Add ui.gutter.selected option for themes (#3303) ... * add `ui.gutter.selected` * add `ui.gutter`, `ui.gutter.selected` to docs		2022-10-03 23:44:45 +09:00
..
src	Add ui.gutter.selected option for themes (#3303)	2022-10-03 23:44:45 +09:00
theme	fix typos (#2304)	2022-04-27 14:21:20 -05:00
.gitignore	Add book/ (mdbook based user guide)	2021-04-05 15:48:08 +09:00
book.toml	Improve docs, fix up a few highlight scopes	2021-09-07 13:03:48 +09:00