enabling pulls again in dev branch

diff --git a/scripts/rev_control/version_control.sh b/scripts/rev_control/version_control.sh
index 8c714ece4974d0269ef4b8b13b715dd7e386a4d9..45da63255334528f9b601ad1db61e25380a73b9e 100644 (file)
--- a/scripts/rev_control/version_control.sh
+++ b/scripts/rev_control/version_control.sh
@@ -279,15 +279,16 @@ else
     echo "Diverged"
 fi
 
-echo The rest of pull is not being done yet.
-return 1
-
   # now pull down any changes in our own origin in the repo, to stay in synch
   # with any changes from others.
-  git pull --no-ff origin
+  git pull --no-ff --all
   test_or_die "git fetch origin"
 
 
+echo The rest of pull is not being done yet.
+return 1
+
+
 
 # below has older shards of partial knowledge.