Minor documentation updates

[pintos-anon] / doc / localsettings.texi

diff --git a/doc/localsettings.texi b/doc/localsettings.texi
index 4f061595d860e446bad1a7f4de1865458ab0d23f..3e41b8b1f7a4f0c0f3d44eadebc7d02a521a2c27 100644 (file)
--- a/doc/localsettings.texi
+++ b/doc/localsettings.texi
@@ -1,6 +1,5 @@
 @c Local settings
 
-@set coursenumber CS 140
 @set localpintostarpath /usr/class/cs140/pintos/pintos.tar.gz
 @set localpintoshttppath http://@/www.stanford.edu/@/class/@/cs140/@/pintos/@/pintos.@/tar.gz
 @set localpintosbindir /usr/class/cs140/`uname -m`/bin
@@ -17,8 +16,8 @@ ITSS webpage}.  You may use the Solaris or Linux machines.
 
 @macro localpathsetup{}
 Under @command{csh}, Stanford's login shell, you can do so
-with this command:@footnote{The term @samp{`uname -m`} expands to either
-@file{sun4u} or @file{i686} according to the type of computer you're
+with this command:@footnote{The term @samp{`uname -m`} expands to a value
+such as @file{x86_64} that indicates the type of computer you're
 logged into.}
 @example
 set path = ( @value{localpintosbindir} $path )