Pintos: pintos/src/tests/main.c Source File

00001 #include <random.h>
00002 //3213394286
00003 #include "tests/lib.h"
00004 #include "tests/main.h"
00005 
00006 int
00007 main (int argc UNUSED, char *argv[]) 
00008 {
00009   test_name = argv[0];
00010 
00011   msg ("begin");
00012   random_init (0);
00013   test_main ();
00014   msg ("end");
00015   return 0;
00016 }