UserPreferences.st
changeset 21234 5484b13cded1
parent 21125 aa7155bed06e
child 21235 4859f3fef7ca
--- a/UserPreferences.st	Thu Jan 12 10:06:29 2017 +0100
+++ b/UserPreferences.st	Thu Jan 12 15:01:03 2017 +0100
@@ -4069,6 +4069,18 @@
     self 
         at: #'history-manager.allow-edit-of-history'
         put:aBoolean
+!
+
+historyManagerEnabled
+    ^self 
+        at: #'history-manager.enabled'
+        ifAbsent: true 
+!
+
+historyManagerEnabled:aBoolean
+    ^self 
+        at: #'history-manager.enabled'
+        put: aBoolean 
 ! !
 
 !UserPreferences methodsFor:'accessing-prefs-code'!