--- a/UserPreferences.st Mon Dec 10 20:44:40 2018 +0100
+++ b/UserPreferences.st Tue Dec 11 18:32:30 2018 +0100
@@ -946,8 +946,6 @@
^ modified ? false
! !
-
-
!UserPreferences methodsFor:'accessing-locale'!
dateInputFormat
@@ -1716,7 +1714,6 @@
^ DiffCodeView
! !
-
!UserPreferences methodsFor:'accessing-prefs-UI'!
allowMouseWheelZoom
@@ -3879,6 +3876,15 @@
"Modified: / 1.4.1998 / 13:25:06 / cg"
!
+fullSelectorCheck:aBoolean
+ "with fullSelector check, selectors are searched immediately for
+ being implemented in the system. This may not be useful on slow machines"
+
+ self at:#fullSelectorCheck put:aBoolean
+
+ "Created: / 11-12-2018 / 18:31:48 / Claus Gittinger"
+!
+
globalClassIdentifierColor
"the color used for global identifiers which are known to be classes;
If syntaxColoring is turned on."