From: Ben Pfaff Date: Wed, 5 Apr 2006 20:09:13 +0000 (+0000) Subject: Add section heading for Debugging User Programs. X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=1efa390f39175f3c37c43ed0fbc4e3f78900a78d;p=pintos-anon Add section heading for Debugging User Programs. Thanks to "Huey Kwik" for the question. --- diff --git a/doc/debug.texi b/doc/debug.texi index ce3e4bd..ba53f70 100644 --- a/doc/debug.texi +++ b/doc/debug.texi @@ -314,7 +314,13 @@ a bug in the original Pintos code. The first and second are quite likely, and you should seriously consider both. We hope that the third is less likely, but it is also possible. -@anchor{Debugging User Programs} +@menu +* Debugging User Programs:: +@end menu + +@node Debugging User Programs +@subsection Debugging User Programs + You can also use @command{gdb} to debug a user program running under Pintos. Start by issuing this @command{gdb} command to load the program's symbol table: