--- 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