diff options
| author | David Aspinall | 1998-10-07 17:50:46 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-10-07 17:50:46 +0000 |
| commit | 832708eef18b26052bf56b2064ba1846e68c1891 (patch) | |
| tree | 52fcb9d6273876f571bf2ba1e54664e630cecb89 | |
| parent | 518849bff31120315f85cd87b368618c19aeee19 (diff) | |
Disabeled remote release
| -rw-r--r-- | Makefile.devel | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/Makefile.devel b/Makefile.devel index e47a3504..90041bdc 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -39,9 +39,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 -CVS_RSH=ssh +# MACHINE=hope +# CVSROOT = :ext:$(USER)@$(MACHINE).dcs.ed.ac.uk:/home/proofgen/src +# CVS_RSH=ssh +CVSROOT = /home/proofgen/src # Byte compilation command |