X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fdevel.texi;h=60851dfe1d9334a4ec7546780e21907dbdda7398;hb=5dedd25ecab2a6ade0e5a98f86b4134e13176e37;hp=061f2fda177fcaa1bfbb528672eb018e4c4f086f;hpb=62cb7e093d2062b44c04663e8bfb9c225e21ae4f;p=pintos-anon

diff --git a/doc/devel.texi b/doc/devel.texi
index 061f2fd..60851df 100644
--- a/doc/devel.texi
+++ b/doc/devel.texi
@@ -49,6 +49,7 @@ home page}.
 @menu
 * Setting Up CVS::              
 * Using CVS::                   
+* CVS Locking::                 
 @end menu
 
 @node Setting Up CVS