93f3e054ae5c36a657f964ad89b4bb246f15119b
max
  Fri Jun 20 06:28:03 2025 -0700
I think there is a git pull missing in the push script

diff --git build/doPush.sh build/doPush.sh
index d4c09e5..00fe250 100755
--- build/doPush.sh
+++ build/doPush.sh
@@ -1,11 +1,12 @@
 #!/bin/sh -e
 
 git checkout master
+git pull
 git merge develop
 git push
 git tag $CBVERSION
 git push origin $CBVERSION
 
 # this assumes that build is a child of the top level directory
 cd ..
 make pip