X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pintos-anon;a=blobdiff_plain;f=doc%2Fdevel.texi;h=eae54d163956de002a61f1d78424326704c31509;hp=ea024c164404d280f4e520ac4301e1d13407d037;hb=5af653aea4f817d41de3d2ab3a9eeaec44016234;hpb=401069bc9a5b60287a21798f8a69c2f1c84dcba7

diff --git a/doc/devel.texi b/doc/devel.texi
index ea024c1..eae54d1 100644
--- a/doc/devel.texi
+++ b/doc/devel.texi
@@ -6,12 +6,16 @@ Here are some tools that you might find useful while developing code.
 @menu
 * Tags::
 * cscope::
-* CVS:: @ifset recommendsourceforge 
-* SourceForge:: @end ifset 
+* CVS::
+@ifset recommendsourceforge 
+* SourceForge::
+@end ifset 
 @ifset recommendvnc
-* VNC:: @end ifset 
+* VNC::
+@end ifset 
 @ifset recommendcygwin
-* Cygwin:: @end ifset
+* Cygwin::
+@end ifset
 @end menu
 
 @node Tags