Fix up header guards.
[pintos-anon] / src / lib / random.h
index cc6eed41bf28f0788c0be709bae1d21754c59130..0950ae2e0e76f54f6f018c457d14d6a3e2daf5e0 100644 (file)
@@ -1,5 +1,5 @@
-#ifndef HEADER_RANDOM_H
-#define HEADER_RANDOM_H 1
+#ifndef __LIB_RANDOM_H
+#define __LIB_RANDOM_H
 
 #include <stddef.h>
 
@@ -7,4 +7,4 @@ void random_init (unsigned seed);
 void random_bytes (void *, size_t);
 unsigned long random_ulong (void);
 
-#endif /* random.h */
+#endif /* lib/random.h */