X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;ds=sidebyside;f=src%2Fuserprog%2Faddrspace.c;h=28e89f7884ec2d5245ded6c056bddfe3b9fa885d;hb=76a72158378a6447bb3dbce5bae41db48da0d64f;hp=3837d4ed00a6e6edce942bdd2dcd25840041acee;hpb=a98578bf3b6b5c946713654b404a886a7199dbee;p=pintos-anon

diff --git a/src/userprog/addrspace.c b/src/userprog/addrspace.c
index 3837d4e..28e89f7 100644
--- a/src/userprog/addrspace.c
+++ b/src/userprog/addrspace.c
@@ -230,3 +230,12 @@ addrspace_destroy (struct addrspace *as)
   if (as != NULL && as->pagedir != NULL) 
     pagedir_destroy (as->pagedir); 
 }
+
+void
+addrspace_activate (struct addrspace *as) 
+{
+  ASSERT (as != NULL);
+  
+  if (as->pagedir != NULL)
+    pagedir_activate (as->pagedir);
+}