From a0095cd01075664d4b692bd84203f319acb23d02 Mon Sep 17 00:00:00 2001
From: Chris Koeritz <fred@gruntose.com>
Date: Fri, 10 Nov 2017 11:15:28 -0500
Subject: [PATCH] arghsomeness

---
 scripts/rev_control/version_control.sh | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/scripts/rev_control/version_control.sh b/scripts/rev_control/version_control.sh
index 718b602c..3c6685d6 100644
--- 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)
-- 
2.34.1