diff options
Diffstat (limited to 'ide/preferences.ml')
| -rw-r--r-- | ide/preferences.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index abfa1857e..80caefa5f 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -158,8 +158,8 @@ let (current:pref ref) = vertical_tabs = false; opposite_tabs = false; - processing_color = "light green"; - processed_color = "light blue"; + processed_color = "light green"; + processing_color = "light blue"; } |