diff options
| author | Ivan Tham | 2022-07-18 01:13:47 +0000 |
|---|---|---|
| committer | GitHub | 2022-07-18 01:13:47 +0000 |
| commit | e8214fb1e6009d44a4b7094c6e5297a19f18f549 (patch) | |
| tree | 1dc2dc1b15f3ed675dd7fed78632b2a0a08bccee /runtime/queries/regex | |
| parent | 2a8d38c27bce34c9b6fa95a2fb063fe097e220d4 (diff) | |
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.
Diffstat (limited to 'runtime/queries/regex')
0 files changed, 0 insertions, 0 deletions