From: Ben Pfaff <blp@cs.stanford.edu>
Date: Wed, 8 Sep 2004 00:08:35 +0000 (+0000)
Subject: Update name to Pintos.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=d0d14ca50fbac167253e1e1d8d806bfd749a5e8a;p=pintos-anon

Update name to Pintos.
---

diff --git a/src/threads/init.c b/src/threads/init.c
index 35ce92a..729c25f 100644
--- 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 ();