Ivan Tham e8214fb1e6 Make gutters padding optional (#2996) ... If all gutters are removed, there are still an extra one padding, would be nice to remove that to save some space.		2022-07-18 10:13:47 +09:00
..
src	Make gutters padding optional (#2996)	2022-07-18 10:13:47 +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