X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fuserprog.texi;h=a1321950fd3f877328f801853839be7c9cf69741;hb=abb75db6729325ad6210f6e8e8043b720b5e0180;hp=cf01158423f9540ce0d91bf7aa3c745d00d71709;hpb=45716d7c0001861ebf8848217cdc446c4ba2c47a;p=pintos-anon

diff --git a/doc/userprog.texi b/doc/userprog.texi
index cf01158..a132195 100644
--- a/doc/userprog.texi
+++ b/doc/userprog.texi
@@ -924,7 +924,7 @@ Modify @file{src/examples/Makefile}, then run @command{make}.
 
 @item Can I run user programs under a debugger?
 
-Yes, with some limitations.  @xref{Debugging User Programs}.
+Yes, with some limitations.  @xref{GDB}.
 
 @item What's the difference between @code{tid_t} and @code{pid_t}?