X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fdebug.texi;h=12ca40ee3641017fffd269c40a10c25a3a8625c8;hb=f6d77b49fb7e4bab34c7fa4dc1ae9cd307231e23;hp=cf8edc040029784e39feab449277678364e20cb5;hpb=7a3a3477d2001ebb9b8c73e4785f16d47788f52c;p=pintos-anon

diff --git a/doc/debug.texi b/doc/debug.texi
index cf8edc0..12ca40e 100644
--- a/doc/debug.texi
+++ b/doc/debug.texi
@@ -256,7 +256,7 @@ backtrace kernel.o Call stack: 0xc0106eff 0xc01102fb 0xc010dc22
 You can run the Pintos kernel under the supervision of the
 @command{i386-elf-gdb} debugger.@footnote{If you're using an
 80@var{x}86 system for development, it's probably just called
-@command{addr2line}.}  There are two steps in the process.  First,
+@command{gdb}.}  There are two steps in the process.  First,
 start Pintos with the @option{--gdb} option, e.g.@: @command{pintos
 --gdb run}.  Second, in a second terminal, invoke @command{gdb} on
 @file{kernel.o}: