X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fdevel.texi;h=48ed58d46e2f2a95f654c2431fba02cc5d77b0d5;hb=672f483fb765ec387f12d8933b120a7306831d70;hp=061f2fda177fcaa1bfbb528672eb018e4c4f086f;hpb=6c06e2792f47c13fff2bb3832ca81f3762038493;p=pintos-anon

diff --git a/doc/devel.texi b/doc/devel.texi
index 061f2fd..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.
@@ -49,6 +49,7 @@ home page}.
 @menu
 * Setting Up CVS::              
 * Using CVS::                   
+* CVS Locking::                 
 @end menu
 
 @node Setting Up CVS