If we're seeing failures on this test, they need to be investigated. The resume invocation is definitely supposed to call the scheduler and leave with the highest priority thread running.
This "fix" was added before the release in 2014 and I don't have history copy of sel4test, so if anybody remembers what this might have been about, please do comment.
If we're seeing failures on this test, they need to be investigated. The resume invocation is definitely supposed to call the scheduler and leave with the highest priority thread running.
This "fix" was added before the release in 2014 and I don't have history copy of sel4test, so if anybody remembers what this might have been about, please do comment.