Discourage combining student contributions late.

[pintos-anon] / doc / devel.texi

diff --git a/doc/devel.texi b/doc/devel.texi
index 20af12f69b419bdb5ce8df583dc707d995a45cef..86c47f471e7c3cb764cfd1aae939adcc2eeb4a0c 100644 (file)
--- a/doc/devel.texi
+++ b/doc/devel.texi
@@ -6,6 +6,7 @@ Here are some tools that you might find useful while developing code.
 @menu
 * Tags::                        
 * CVS::                         
+* SourceForge::                 
 * VNC::                         
 @end menu
 
@@ -45,6 +46,17 @@ the projects.
 For more information, visit the @uref{https://www.cvshome.org/, , CVS
 home page}.
 
+@node SourceForge
+@section SourceForge
+
+SourceForge is a web-based system for facilitating software
+development.  It provides you with a version-control system (typically
+CVS, as described above) and other tools for tracking your software.
+You can use it to store files, track bugs, and post notes about
+development progress.  It's also free.  You can set up your own
+project in SourceForge at @uref{http://sourceforge.net, ,
+sourceforge.net}.
+
 @node VNC
 @section VNC