UserPreferences.st
changeset 22947 45a2ead06130
parent 22932 9084fa64673e
child 23066 caf3599f703e
--- a/UserPreferences.st	Wed May 16 14:49:43 2018 +0200
+++ b/UserPreferences.st	Wed May 16 15:37:51 2018 +0200
@@ -1623,6 +1623,7 @@
     ^ DiffCodeView
 ! !
 
+
 !UserPreferences methodsFor:'accessing-prefs-UI'!
 
 allowMouseWheelZoom
@@ -4252,6 +4253,13 @@
     self 
         at: #'history-manager.allow-edit-of-history'
         put:aBoolean
+
+    "
+        self default historyManagerAllowEditOfHistory:true.
+        self default historyManagerAllowEditOfHistory:false.
+    "
+
+    "Modified (comment): / 16-05-2018 / 14:24:00 / Stefan Vogel"
 !
 
 historyManagerEnabled