X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pintos-anon;a=blobdiff_plain;f=doc%2Fdevel.texi;h=48ed58d46e2f2a95f654c2431fba02cc5d77b0d5;hp=60851dfe1d9334a4ec7546780e21907dbdda7398;hb=f415a37905c57f61b444806bf84f5405184452aa;hpb=fa97205f611b922b85299e79edba9a0bbbe3cfb2

diff --git a/doc/devel.texi b/doc/devel.texi
index 60851df..48ed58d 100644
--- a/doc/devel.texi
+++ b/doc/devel.texi
@@ -1,4 +1,4 @@
-@node Development Tools, , Debugging Tools, Top
+@node Development Tools
 @appendix Development Tools
 
 Here are some tools that you might find useful while developing code.