diff --git a/apps/sel4test-tests/src/tests/schedcontext.c b/apps/sel4test-tests/src/tests/schedcontext.c index 3d1ed2b4..dc08da95 100644 --- a/apps/sel4test-tests/src/tests/schedcontext.c +++ b/apps/sel4test-tests/src/tests/schedcontext.c @@ -12,9 +12,14 @@ #include "../helpers.h" +/* FIXME: this is a temporary hack and MIN_BUDGET_US should be exported via libsel4 */ #ifndef MIN_BUDGET_US +#ifdef CONFIG_PLAT_TK1 +#define MIN_BUDGET_US (2 * 100) +#else #define MIN_BUDGET_US (2 * 10) #endif +#endif int test_sched_control_configure(env_t env) {