From abeff8ef42e842bf453d20fb8a743ce5653ede0d Mon Sep 17 00:00:00 2001
From: Ben Pfaff <blp@cs.stanford.edu>
Date: Thu, 3 Jul 2008 19:30:05 +0000
Subject: [PATCH] Make recent Texinfo accept devel.texi.

---
 doc/devel.texi | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

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
-- 
2.30.2