Declare argc, argv.
[pintos-anon] / src / threads / init.h
index b4820796255e054e649eb6352b1aa6c6e089719e..e23269de24568962d5d2ba29696e02414bc6f97e 100644 (file)
@@ -3,7 +3,12 @@
 
 #include <stddef.h>
 
+struct tss *tss;
+
 extern size_t kernel_pages;
 extern size_t ram_pages;
 
+extern int argc;
+extern char *argv[];
+
 #endif /* init.h */