diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2017-09-19 23:38:37 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-09-19 23:38:37 +0200 |
| commit | dc7b3c309a3eb7d2c06d24e9a7c34bd84693efdd (patch) | |
| tree | 02853c5073b35f9a375ad0f0628f65716220a61c /editor/plugins/script_text_editor.h | |
| parent | 01e4d2672c3e575da3331536b11f3e96c472fb59 (diff) | |
| parent | 059d00742391d53b9c273c3bd9eefb247db5a4ac (diff) | |
Merge pull request #11310 from djrm/pr_mono_font_in_log
Use code font in editor log
Diffstat (limited to 'editor/plugins/script_text_editor.h')
0 files changed, 0 insertions, 0 deletions