_Scheduler_FIXME_thread_priority_queues_are_broken
Delete this variable since it is no longer necessary due to the thread priority queue implementation change to use RB trees.