Update docs.

[pintos-anon] / doc / devel.texi

diff --git a/doc/devel.texi b/doc/devel.texi
index df5d19685dbeb568d558efe22cb10634247234e2..20af12f69b419bdb5ce8df583dc707d995a45cef 100644 (file)
--- 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