From 42063530c0690f5aa19795019e2598a53e4c836a Mon Sep 17 00:00:00 2001
From: Christian Mehlis <mehlis@inf.fu-berlin.de>
Date: Sun, 9 Jun 2013 17:52:02 +0200
Subject: [PATCH] clarify: while loop without body is correct here

---
 core/sched.c | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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");
     }