X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fintro.texi;h=f22ba76e20b0a187e41002cba3b71cf8ec88e20a;hb=37deefa57e17a299779936ae6d2b74df2e517368;hp=97037eb52473e4692674adbab2fc295cd54623fb;hpb=5e68c020d57d0e8eab14f8cce9b8a1ce1ffddba5;p=pintos-anon

diff --git a/doc/intro.texi b/doc/intro.texi
index 97037eb..f22ba76 100644
--- a/doc/intro.texi
+++ b/doc/intro.texi
@@ -478,9 +478,9 @@ Rosenblum.
 Pintos originated as a replacement for Nachos with a similar design.
 Since then Pintos has greatly diverged from the Nachos design.  Pintos
 differs from Nachos in two important ways.  First, Pintos runs on real
-or simulated 80@var{x}86 hardware, whereas Nachos runs as a process on a
-host operating system.  Second, like most real-world operating systems,
-Pintos is written in C, whereas Nachos is written in C++.
+or simulated 80@var{x}86 hardware, but Nachos runs as a process on a
+host operating system.  Second, Pintos is written in C like most
+real-world operating systems, but Nachos is written in C++.
 
 Why the name ``Pintos''?  First, like nachos, pinto beans are a common
 Mexican food.  Second, Pintos is small and a ``pint'' is a small amount.