kernel.(c|h) moved debugging code into if (DEBUGGING) section and cleaned up whitespace

kernel.c

@@ -23,7 +23,7 @@ extern void init()
 
     read_binary_table();
 
-    scheduler_run_next();   
+    scheduler_run_next();
 }
 
 void read_binary_table()
@@ -38,10 +38,14 @@ void read_binary_table()
     for (int i = 0; i < NUM_BINARIES; i++) {
         if (binary_table[i].binid == 0)
             break;
-        // print message
+
-        msg[18] = (char) binary_table[i].binid + '0';
+        if (DEBUGGING) {
-        msg[27] = (char) i + '0';
+            // print message
-        dbgln(msg, 28);
+            msg[18] = (char) binary_table[i].binid + '0';
+            msg[27] = (char) i + '0';
+            dbgln(msg, 28);
+        }
+
         info.allocate_memory_start = binary_table[i].bounds[1];
     }
 

kernel.h

@@ -5,7 +5,7 @@
 #define false 0
 
 #define PROCESS_COUNT 8            // number of concurrent processes
-#define NUM_BINARIES  4            // number of binaries loaded simultaneously 
+#define NUM_BINARIES  4            // number of binaries loaded simultaneously
 
 // scheduler settings
 #define TIME_SLICE_LEN 10          // number of cpu time ticks per slice