From: Ben Pfaff <blp@cs.stanford.edu>
Date: Mon, 20 Sep 2004 04:29:22 +0000 (+0000)
Subject: Comments.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=fed5182e7821669097119fb255c5fd273f68c79e;p=pintos-anon

Comments.
---

diff --git a/src/threads/palloc.c b/src/threads/palloc.c
index 372e528..f00b31e 100644
--- a/src/threads/palloc.c
+++ b/src/threads/palloc.c
@@ -72,10 +72,12 @@ palloc_init (void)
   init_pool (&user_pool, free_middle, free_end, "user pool");
 }
 
-/* Obtains and returns a free page.  If PAL_ZERO is set in FLAGS,
-   then the page is filled with zeros.  If no pages are
-   available, returns a null pointer, unless PAL_ASSERT is set in
-   FLAGS, in which case the kernel panics. */
+/* Obtains and returns a free page.  If PAL_USER is set, the page
+   is obtained from the user pool, otherwise from the kernel
+   pool.  If PAL_ZERO is set in FLAGS, then the page is filled
+   with zeros.  If no pages are available, returns a null
+   pointer, unless PAL_ASSERT is set in FLAGS, in which case the
+   kernel panics. */
 void *
 palloc_get (enum palloc_flags flags)
 {