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