aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/cvs-tips.txt
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2003-05-28 19:41:23 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2003-05-28 19:41:23 +0000
commitd3e17ad5653ee8a47995ab13dcde72179abde440 (patch)
tree4802ba53e21372fe7906103427141c9065d5b659 /etc/cvs-tips.txt
parent6bc0e26b2a13b2ddd393df502ce9f5177894dd71 (diff)
Updated.
Diffstat (limited to 'etc/cvs-tips.txt')
-rw-r--r--etc/cvs-tips.txt9
1 files changed, 5 insertions, 4 deletions
diff --git a/etc/cvs-tips.txt b/etc/cvs-tips.txt
index a8b8fc7f..5566620d 100644
--- a/etc/cvs-tips.txt
+++ b/etc/cvs-tips.txt
@@ -15,10 +15,11 @@ dcs.ed.
your passphrase as needed. The point is that you don't want to
keep typing passwords on every CVS command).
-2. The CVS repository for PG is in ~proofgen/src at dcs.ed.ac.uk To
-use this, you need to set CVSROOT and CVS_RSH. I use the script below
-(the last line isn't essential but makes the settings inside a running
-emacs too)
+2. The CVS repository for PG is in ~proofgen/src at dcs.ed.ac.uk
+
+To use this, you need to set CVSROOT and CVS_RSH. I use the script
+below (the last line isn't essential but makes the settings inside a
+running emacs too)
3. Where you want to develop PG, do: