diff options
| author | Pedro J. Estébanez <pedrojrulez@gmail.com> | 2022-07-24 20:25:34 +0200 |
|---|---|---|
| committer | Pedro J. Estébanez <pedrojrulez@gmail.com> | 2022-07-24 20:25:34 +0200 |
| commit | b96fe1e4bd32f24469edd5bd660ae30ae0c3d1ed (patch) | |
| tree | b7e2943aaeaf10a96cadb8553658945cf216d388 /doc/tools | |
| parent | a5bc65bbadad814a157283749c1ef8552f1663c4 (diff) | |
Mark some editor settings as requiring editor restart
Diffstat (limited to 'doc/tools')
0 files changed, 0 insertions, 0 deletions