projects
/
pintos-anon
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Make recent Texinfo accept devel.texi.
[pintos-anon]
/
doc
/
devel.texi
diff --git
a/doc/devel.texi
b/doc/devel.texi
index ea024c164404d280f4e520ac4301e1d13407d037..eae54d163956de002a61f1d78424326704c31509 100644
(file)
--- 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::
@menu
* Tags::
* cscope::
-* CVS:: @ifset recommendsourceforge
-* SourceForge:: @end ifset
+* CVS::
+@ifset recommendsourceforge
+* SourceForge::
+@end ifset
@ifset recommendvnc
@ifset recommendvnc
-* VNC:: @end ifset
+* VNC::
+@end ifset
@ifset recommendcygwin
@ifset recommendcygwin
-* Cygwin:: @end ifset
+* Cygwin::
+@end ifset
@end menu
@node Tags
@end menu
@node Tags