Update on debug: printing time

executablecode/src/debug.c

 #include <stdlib.h>
 #include <stdio.h>
+#include <time.h>
 
 #include "debug.h"
 
+
 #define DEBUG_ON 1
 #define DEBUG_OFF 2
 
@@ -65,3 +67,7 @@ void debugMsg(char *msg) {
     printf("DT> %s\n", msg);
   }
 }
+
+void debugTime(struct timespec *ts) {
+  printf("DT> sec=%ld nsec=%ld", ts->tv_sec, ts->tv_nsec);
+}

executablecode/src/debug.h

@@ -11,6 +11,7 @@ void debugTwoInts(char *msg, int value1, int value2);
 void debugLong(char *msg, long value);
 void debugInt(char *msg, int value);
 void debugMsg(char *msg);
+void debugTime(struct timespec *ts);
 
 #endif