}
}
-/* If SCHEDULER_MODE is on, then set it back to off. Warn the user
- about the change. */
-
-void
-reset_schedlock (void)
-{
- if (scheduler_mode == schedlock_on)
- {
- warning ("Resetting scheduler-lock mode to 'off'");
- scheduler_mode = schedlock_off;
- }
-}
-
/* True if execution commands resume all threads of all processes by
default; otherwise, resume only threads of the current inferior
process. */