X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fdebug.texi;h=ce3e4bd0a35fb6ff38d70374c3cabfde1bab814e;hb=1c07a79a63dbbd1f4047bf32046518de6f879d50;hp=8fbc7d53bd6b7bdcb16950754de7c47bd8fd70b5;hpb=1a6abd0f04e216d22c57b2cc149c90915eb9f4d1;p=pintos-anon

diff --git a/doc/debug.texi b/doc/debug.texi
index 8fbc7d5..ce3e4bd 100644
--- a/doc/debug.texi
+++ b/doc/debug.texi
@@ -314,6 +314,7 @@ 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}
 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: