add git pull

apalache-mc · Dec 13, 2024 · 7e78e08 · 7e78e08
1 parent 1742832
commit 7e78e08
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/script/release-prepare.sh b/script/release-prepare.sh
@@ -67,6 +67,7 @@ fi
 DEV_VERSION=$("$DIR"/get-version.sh)
 git add --update
 git commit -m "Bump version to ${DEV_VERSION}"
+git pull
 
 instructions="
 # Reviewer instructions