arghsomeness

diff --git a/scripts/rev_control/version_control.sh b/scripts/rev_control/version_control.sh
index 718b602c0cb16fa20799da155fe7032851ddfc3f..3c6685d67ad1fae3a2c4a4c500be88b9345e7338 100644 (file)
--- a/scripts/rev_control/version_control.sh
+++ b/scripts/rev_control/version_control.sh
@@ -294,10 +294,6 @@ function do_update()
       git remote update
       test_or_die "git remote update"
 
-      git pull origin
-#--no-ff 
-      test_or_die "git fetch origin"
-
 # from: https://stackoverflow.com/questions/3258243/check-if-pull-needed-in-git
 UPSTREAM=$(parent_branch_name)
 #argh: original UPSTREAM='${1:-'\''@{u}'\''}'
@@ -316,7 +312,11 @@ else
     echo "Diverged"
 fi
 
-echo The rest of pull is not done yet.
+echo The rest of pull is not being done yet.
+return 1
+
+      git pull --no-ff origin
+      test_or_die "git fetch origin"
 
 
 #      reslog=$(git log HEAD..origin/master --oneline)