Update docs.

[pintos-anon] / doc / debug.texi

diff --git a/doc/debug.texi b/doc/debug.texi
index d48e6392e477f7da88f33363b59abba690056da4..82f001ffbe91ffbdb2dedc912c4c08f202ba6059 100644 (file)
--- a/doc/debug.texi
+++ b/doc/debug.texi
@@ -16,7 +16,7 @@ introduces you to a few of them.
 @end menu
 
 @node printf
-@section @func{printf}
+@section @code{@code{printf()}}
 
 Don't underestimate the value of @func{printf}.  The way
 @func{printf} is implemented in Pintos, you can call it from