X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fdebug.texi;h=82f001ffbe91ffbdb2dedc912c4c08f202ba6059;hb=1b504c481511634620ba35628f2ef991a9f9f3c0;hp=d48e6392e477f7da88f33363b59abba690056da4;hpb=36088b8cdcd561b472b60ae5e9cf7a5fde9132b9;p=pintos-anon

diff --git a/doc/debug.texi b/doc/debug.texi
index d48e639..82f001f 100644
--- 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