Minor documentation updates
[pintos-anon] / doc / userprog.texi
index cf01158423f9540ce0d91bf7aa3c745d00d71709..7d734c616109ef741fade27dcc422de77dbf40c8 100644 (file)
@@ -261,7 +261,7 @@ processor's floating-point unit when switching threads.
 
 The @file{src/examples} directory contains a few sample user
 programs.  The @file{Makefile} in this directory
-compiles the provided examples, and you can edit it
+compiles the provided examples, and you can edit it to
 compile your own programs as well.  Some of the example programs will
 only work once projects 3 or 4 have been implemented.
 
@@ -600,8 +600,8 @@ programs only.)  System call numbers for each system call are defined in
 @file{lib/syscall-nr.h}:
 
 @deftypefn {System Call} void halt (void)
-Terminates Pintos by calling @func{power_off} (declared in
-@file{threads/init.h}).  This should be seldom used, because you lose
+Terminates Pintos by calling @func{shutdown_power_off} (declared in
+@file{devices/shutdown.h}).  This should be seldom used, because you lose
 some information about possible deadlock situations, etc.
 @end deftypefn
 
@@ -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}?