diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2018-12-12 08:31:31 +0100 |
|---|---|---|
| committer | Rémi Verschelde <rverschelde@gmail.com> | 2018-12-12 08:31:31 +0100 |
| commit | 77dd0561ef0ad508878ce2899d5181e9c9b632d6 (patch) | |
| tree | be661558a619c48b54fc515ec97da2a86c44452c /misc/scripts/compare_extension_api.py | |
| parent | fe68f53298a28d3fbc159a92e48ef2971a8467ae (diff) | |
EditorSettings: Remove unused settings from initial set
Fixes #24291.
Diffstat (limited to 'misc/scripts/compare_extension_api.py')
0 files changed, 0 insertions, 0 deletions