Rename addrspace to process.
[pintos-anon] / src / userprog / addrspace.h
diff --git a/src/userprog/addrspace.h b/src/userprog/addrspace.h
deleted file mode 100644 (file)
index 6e3b584..0000000
+++ /dev/null
@@ -1,10 +0,0 @@
-#ifndef USERPROG_ADDRSPACE_H
-#define USERPROG_ADDRSPACE_H
-
-#include "threads/thread.h"
-
-tid_t addrspace_execute (const char *filename);
-void addrspace_destroy (struct thread *);
-void addrspace_activate (void);
-
-#endif /* userprog/addrspace.h */