diff options
| author | David Aspinall | 1998-10-07 17:33:40 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-10-07 17:33:40 +0000 |
| commit | 518849bff31120315f85cd87b368618c19aeee19 (patch) | |
| tree | 5678fa794d01ca0e486d6b3a36b86f7d94f13b04 /Makefile.devel | |
| parent | f5901e7bff6734bd4ae661c71e4d344ab28fa13a (diff) | |
Removed ssh.dcs.ed.ac.uk from remote release.
Diffstat (limited to 'Makefile.devel')
| -rw-r--r-- | Makefile.devel | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile.devel b/Makefile.devel index a6b7fee4..e47a3504 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -39,7 +39,8 @@ CVSNAME = ProofGeneral # Remote commands to use CVS in server mode and install files. # With these settings the build can be done remotely. -CVSROOT = :ext:$(USER)@ssh.dcs.ed.ac.uk:/home/proofgen/src +MACHINE=hope +CVSROOT = :ext:$(USER)@$(MACHINE).dcs.ed.ac.uk:/home/proofgen/src CVS_RSH=ssh |