diff options
| author | Rémi Verschelde <remi@verschelde.fr> | 2022-08-25 19:33:06 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-08-25 19:33:06 +0200 |
| commit | 03ec5d7005067517d608b4f5328675b9a0e17486 (patch) | |
| tree | 905db360e5461046e2c33a3217ab9879e42c3f3b /core/os | |
| parent | 5d78ab43888a565a87175814c94cf7d03d8fccb7 (diff) | |
| parent | 517220f6d4addc9f89531022bcbc0e92d25a3860 (diff) | |
Merge pull request #64891 from Calinou/doc-editorsettings-code-font
Fix outdated mentions of default code font in EditorSettings documentation
Diffstat (limited to 'core/os')
0 files changed, 0 insertions, 0 deletions