Update name to Pintos.

diff --git a/src/threads/init.c b/src/threads/init.c
index 35ce92a2e255c7b68865931877dba832c9ff048a..729c25ffcd528957ea96e5f22cf2cf1a439d2cfb 100644 (file)
--- a/src/threads/init.c
+++ b/src/threads/init.c
@@ -58,7 +58,7 @@ main (void)
   serial_init_poll ();
 
   /* Greet user. */
-  printf ("Booting cnachos86 with %'d kB RAM...\n", ram_pages * 4);
+  printf ("Pintos booting with %'d kB RAM...\n", ram_pages * 4);
 
   /* Parse command line. */
   argv_init ();