X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pintos-anon;a=blobdiff_plain;f=doc%2Finstallation.texi;fp=doc%2Finstallation.texi;h=5e35e8b2e0f82240715b09b39a37bec42633baf0;hp=3bab217515767b57ef4547c4593f0aba17dca8b5;hb=4dbef14e57eebfd86079fcc2185adc33e72e2d8b;hpb=5a63c2f04edb9e892275a9ef184878be19cf5ebd

diff --git a/doc/installation.texi b/doc/installation.texi
index 3bab217..5e35e8b 100644
--- a/doc/installation.texi
+++ b/doc/installation.texi
@@ -79,12 +79,12 @@ described below (@pxref{Building Bochs for Pintos}).
 
 @item
 Install scripts from @file{src/utils}.  Copy @file{backtrace},
-@command{pintos}, @command{pintos-gdb}, @command{pintos-mkdisk} into the
+@file{pintos}, @file{pintos-gdb}, @file{pintos-mkdisk} into the
 default @env{PATH}.
 
 @item 
 Install @file{src/misc/gdb-macros} in a public location.  Then use a
-text editor to edit the installed copy of @command{pintos-gdb}, changing
+text editor to edit the installed copy of @file{pintos-gdb}, changing
 the definition of @env{GDBMACROS} to point to where you installed
 @file{gdb-macros}.  Test the installation by running
 @command{pintos-gdb} without any arguments.  If it does not complain