diff --git a/core/sched.c b/core/sched.c
index 0b21dea1f8..2a475b2817 100644
--- a/core/sched.c
+++ b/core/sched.c
@@ -96,7 +96,10 @@ void sched_run() {
 
     if (num_tasks == 0) {
         DEBUG("scheduler: no tasks left.\n");
-        while(! num_tasks);
+        while(! num_tasks) {
+          /* loop until a new task arrives */
+          ;
+        }
         DEBUG("scheduler: new task created.\n");
     }