X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fdevel.texi;h=20af12f69b419bdb5ce8df583dc707d995a45cef;hb=a6200ce9b1944598ab84b804663f068fdf0ede30;hp=df5d19685dbeb568d558efe22cb10634247234e2;hpb=64f9dd66983134b6b95ad2efffdac49323d04835;p=pintos-anon

diff --git a/doc/devel.texi b/doc/devel.texi
index df5d196..20af12f 100644
--- a/doc/devel.texi
+++ b/doc/devel.texi
@@ -1,8 +1,14 @@
-@node Development Tools
+@node Development Tools, , Debugging Tools, Top
 @appendix Development Tools
 
 Here are some tools that you might find useful while developing code.
 
+@menu
+* Tags::                        
+* CVS::                         
+* VNC::                         
+@end menu
+
 @node Tags
 @section Tags