diff options
| author | David Aspinall | 1999-06-28 18:33:51 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-06-28 18:33:51 +0000 |
| commit | f67293ef4c6d37f3bf5b221685bd87bcea8836d4 (patch) | |
| tree | fe55b5249d01edbdfa6556c9f9c11ccc55d56642 | |
| parent | 22bb7abb06f1b74df383835aac0db4fd71837971 (diff) | |
Set CVSROOT for remote cvs.
| -rw-r--r-- | Makefile.devel | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.devel b/Makefile.devel index d9e3162c..fd73d787 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -86,10 +86,10 @@ CVSNAME = ProofGeneral # Remote commands to use CVS in server mode and install files. # With these settings the build can be done remotely. -# MACHINE=hope # CVSROOT = :ext:$(USER)@$(MACHINE).dcs.ed.ac.uk:/home/proofgen/src +# CVSROOT = /home/proofgen/src # CVS_RSH=ssh -CVSROOT = /home/proofgen/src +CVSROOT = :ext:da@scar.dcs.ed.ac.uk:/home/proofgen/src # Emacs EMACS=xemacs |