UserPreferences.st
changeset 23560 2acf26b7ed90
parent 23468 baa19fa832c7
child 23608 4b263e7e24c1
--- 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."