diff options
| -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 |