diff -r e22952cec018 -r 13fd8759f981 Preferences/ConfigurationPages/EditorStylesPage.py --- a/Preferences/ConfigurationPages/EditorStylesPage.py Sun May 06 15:23:02 2018 +0200 +++ b/Preferences/ConfigurationPages/EditorStylesPage.py Mon May 07 19:32:49 2018 +0200 @@ -224,6 +224,8 @@ self.changeMarkerSavedColorButton, Preferences.getEditorColour) + self.markerMapRightCheckBox.setChecked( + Preferences.getEditor("ShowMarkerMapOnRight")) self.initColour("BookmarksMap", self.bookmarksMapButton, Preferences.getEditorColour) @@ -354,6 +356,10 @@ "IndentationGuides", self.indentguidesCheckBox.isChecked()) + Preferences.setEditor( + "ShowMarkerMapOnRight", + self.markerMapRightCheckBox.isChecked()) + self.saveColours(Preferences.setEditorColour) for key in list(self.editorColours.keys()): Preferences.setEditorColour(key, self.editorColours[key])