Change to random call so it will work on linux

diff --git a/Robust/src/Runtime/option.c b/Robust/src/Runtime/option.c
index d1500d630cccade0065214f5910416e72ed9eeaa..552f996447fc8c30d11510b7a973f4aba4fd0181 100644 (file)
--- a/Robust/src/Runtime/option.c
+++ b/Robust/src/Runtime/option.c
@@ -1,6 +1,7 @@
 #include "option.h"
 #include <stdio.h>
 #include <string.h>
+#include <stdlib.h>
 #include "runtime.h"
 
 extern char *options;
@@ -71,7 +72,7 @@ void processOptions() {
       options=strchr(options,' ');
       if (options!=NULL) options++;
       printf("Initializing random number generator.\n");
-      srandomdev();
+      srandom(time(NULL));
     } else
       break;
   }