Mention that aklog and/or logging out and back in may be necessary to

gain new group membership.

diff --git a/doc/devel.texi b/doc/devel.texi
index ece70a9a17381fa2d6add1e4affdf4d8bb1adf05..1aff0655940c6293c7d2adb41205eec7bf41eef7 100644 (file)
--- a/doc/devel.texi
+++ b/doc/devel.texi
@@ -121,10 +121,15 @@ hand, and you should definitely not modify them yourself.
 @subsection Using CVS
 
 To use CVS, start by check out a working copy of the contents of the
-CVS repository into a directory named @file{@var{dir}}, execute
+CVS repository into a directory named @file{@var{dir}}.  To do so, execute
 @samp{cvs -d ~@var{keeper}/cvs checkout -d @var{dir} pintos}, where
 @var{keeper} is the CVS keeper's Leland username.
 
+(If this fails due to some kind of permission problem, then run
+@command{aklog} and try again.  If it still doesn't work, log out and
+back in.  If that still doesn't fix the problem, the CVS repository may
+not be initialized properly.)
+
 At this point, you can modify any of the files in the working copy.
 You can see the changes you've made with @samp{cvs diff -u}.  If you
 want to commit these changes back to the repository, making them