mirror of
https://github.com/genodelabs/genode.git
synced 2025-05-29 05:34:23 +00:00
f74962bdad
The scheduler did not consider the consumed quota during a call to "update" if the head that consumed the quota was removed from the scheduler. When this occured, the internal round time did not advance as expected but remained at its previous value untile the next call to "update" (without a removed head) This commit introduces a new flag that is set only when the head gets removed in order to detect and handle the situation correctly on the next call to "update". Ref #4151 Ref #4710