diff options
| author | Rémi Verschelde <remi@verschelde.fr> | 2016-09-07 20:42:36 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2016-09-07 20:42:36 +0200 |
| commit | 19bd661a8fdc381bb68018028bf76997cf74b65a (patch) | |
| tree | 007a42b8a23750ad9b886a349bd17fcd77155efb /tools/editor_fonts | |
| parent | a40309b53261f4b8fdba1de2cbd6e08e57352be5 (diff) | |
| parent | 9e92fcaef989f9a368dd26cffd38a45deffbb601 (diff) | |
Merge pull request #6421 from Paulb23/highlight_current_script_issue_5450
Added setting to change current script background color, issue 5450
Diffstat (limited to 'tools/editor_fonts')
0 files changed, 0 insertions, 0 deletions