mirror of
https://github.com/arduino/Arduino.git
synced 2025-01-18 07:52:14 +01:00
Restored background color when switching off "external editor" flag in preferences. Fixes #3197
This commit is contained in:
parent
e8eb06aa17
commit
67b65ddd77
@ -477,14 +477,13 @@ public class Editor extends JFrame implements RunnerListener {
|
||||
|
||||
if (external) {
|
||||
// disable line highlight and turn off the caret when disabling
|
||||
Color color = Theme.getColor("editor.external.bgcolor");
|
||||
textarea.setBackground(color);
|
||||
textarea.setBackground(Theme.getColor("editor.external.bgcolor"));
|
||||
textarea.setHighlightCurrentLine(false);
|
||||
textarea.setEditable(false);
|
||||
|
||||
} else {
|
||||
boolean highlight = PreferencesData.getBoolean("editor.linehighlight");
|
||||
textarea.setHighlightCurrentLine(highlight);
|
||||
textarea.setBackground(Theme.getColor("editor.bgcolor"));
|
||||
textarea.setHighlightCurrentLine(PreferencesData.getBoolean("editor.linehighlight"));
|
||||
textarea.setEditable(true);
|
||||
}
|
||||
|
||||
|
Loading…
x
Reference in New Issue
Block a user