mirror of
https://github.com/genodelabs/genode.git
synced 2025-02-21 10:01:57 +00:00
Setting the _need_to_schedule member in the 'ready' method of the scheduler was not done correctly. At least, the _need_to_schedule was set true in situations were the head was not outdated by the 'ready' operation. Ref #4151