1 files changed, 10 insertions, 0 deletions
diff --git a/pintos-progos/lib/random.h b/pintos-progos/lib/random.h
new file mode 100644
index 0000000..0950ae2
--- /dev/null
+++ b/pintos-progos/lib/random.h
@@ -0,0 +1,10 @@
+#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 new file mode 100644 index 0000000..0950ae2 --- /dev/null +++ b/pintos-progos/lib/random.h
@@ -0,0 +1,10 @@
	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 */