remove git pull

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