From: John Ousterhout <ouster@cs.stanford.edu>
Date: Thu, 17 Dec 2015 17:41:53 +0000 (-0800)
Subject: Switch docs to use Git instead of CVS by default
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=5999404c2b4cec0c27676a7fc81596662875aea5;hp=5999404c2b4cec0c27676a7fc81596662875aea5;p=pintos-anon

Switch docs to use Git instead of CVS by default

Also a few minor changes to localsettings.texi.
---