diff options
| author | Rémi Verschelde <remi@verschelde.fr> | 2016-10-30 12:17:28 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2016-10-30 12:17:28 +0100 |
| commit | 914015f3b63dd956e72ea937d46ea4b2db005ada (patch) | |
| tree | 9c1f1b641f9d83e59065140e1ad112d33836a894 /tools/editor/doc_code_font.h | |
| parent | 21828209ec04807c9539dd5acc20de7d14033f37 (diff) | |
| parent | 13c92099e64ddf19978f8a53c66d3e44f5ec5922 (diff) | |
Merge pull request #6962 from henriquelalves/external_editor_focus_bug
Won't change editor tabs when using External Editor.
Diffstat (limited to 'tools/editor/doc_code_font.h')
0 files changed, 0 insertions, 0 deletions