make-shared-reop: allow default server to be overriden by environment

Just set SERVER in the environment prior to calling make-shared-repo
to push to a different server (or with a different user).

1 files changed, 4 insertions, 1 deletions

diff --git a/make-shared-repo b/make-shared-repo
index 13fd039..d0df8a9 100755
--- a/make-shared-repo
+++ b/make-shared-repo
@@ -9,7 +9,10 @@ REPO=`basename "$1"`
 
 # where to copy it to
 REMOTE_PATH="/cvs/proj/litmus/repo/${REPO}.git"
-SERVER="cvs.cs.unc.edu"
+if [ -z "$SERVER" ]
+then
+    SERVER="cvs.cs.unc.edu"
+fi
 
 # command to execute after repository creation
 CHMOD="/cvs/proj/litmus/sw/bin/set_repo_rights --quiet"