projects / pintos-anon / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3d30b9f) | patch
Switch docs to use Git instead of CVS by default
authorJohn Ousterhout <ouster@cs.stanford.edu>
Thu, 17 Dec 2015 17:41:53 +0000 (09:41 -0800)
committerJohn Ousterhout <ouster@cs.stanford.edu>
Thu, 17 Dec 2015 17:41:53 +0000 (09:41 -0800)
commit78eeb7122de7d0df2a5f37fc3b834b54e9bcf91d
treeaecd742ed440350a2ac83cc399021fe2d50fe99etree | snapshot
parent3d30b9f53e93e7a29706118e74bddd91347c595ecommit | diff
Switch docs to use Git instead of CVS by default

Also a few minor changes to localsettings.texi.
doc/devel.texi diff | blob | history
doc/intro.texi diff | blob | history
doc/localsettings.texi diff | blob | history
Pintos public repository