1 files changed, 0 insertions, 10 deletions
diff --git a/pintos-progos/lib/random.h b/pintos-progos/lib/random.h
deleted file mode 100644
index 0950ae2..0000000
--- a/pintos-progos/lib/random.h
+++ /dev/null
@@ -1,10 +0,0 @@
-#ifndef __LIB_RANDOM_H
-#define __LIB_RANDOM_H
-#include <stddef.h>
-void random_init (unsigned seed);
-void random_bytes (void *, size_t);
-unsigned long random_ulong (void);
-#endif /* lib/random.h */

diff --git a/pintos-progos/lib/random.h b/pintos-progos/lib/random.h deleted file mode 100644 index 0950ae2..0000000 --- a/pintos-progos/lib/random.h +++ /dev/null
@@ -1,10 +0,0 @@
1	#ifndef __LIB_RANDOM_H
2	#define __LIB_RANDOM_H
3
4	#include <stddef.h>
5
6	void random_init (unsigned seed);
7	void random_bytes (void *, size_t);
8	unsigned long random_ulong (void);
9
10	#endif /* lib/random.h */