No longer recommend SourceForge.

[pintos-anon] / doc / localsettings.texi

diff --git a/doc/localsettings.texi b/doc/localsettings.texi
index e8bb45b07e3a61f18c2e5ec31d0a1c1c20b07fba..4f061595d860e446bad1a7f4de1865458ab0d23f 100644 (file)
--- a/doc/localsettings.texi
+++ b/doc/localsettings.texi
@@ -5,7 +5,6 @@
 @set localpintoshttppath http://@/www.stanford.edu/@/class/@/cs140/@/pintos/@/pintos.@/tar.gz
 @set localpintosbindir /usr/class/cs140/`uname -m`/bin
 
-@set recommendsourceforge
 @set recommendvnc
 @clear recommendcygwin
 
@@ -58,8 +57,7 @@ inspired your own in your design documentation.
 
 @macro localcvspolicy{}
 Instead, we recommend integrating your team's changes early and often,
-using a source code control system such as CVS (@pxref{CVS}) or a
-group collaboration site such as SourceForge (@pxref{SourceForge}).
+using a source code control system such as CVS (@pxref{CVS}).
 This is less likely to produce surprises, because everyone can see
 everyone else's code as it is written, instead of just when it is
 finished.  These systems also make it possible to review changes and,