Missed a reference to the default branch (#708)

runtimeverification · Jul 18, 2024 · 9c03323 · 9c03323
1 parent 3244fe8
commit 9c03323
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.github/workflows/master-push.yml b/.github/workflows/master-push.yml
@@ -30,7 +30,7 @@ jobs:
           new_master="$(git rev-parse origin/master)"
           
           if git diff --exit-code ${old_master} ${new_master} -- package/version; then
-            og_version=$(git show origin/${GITHUB_BASE_REF}:package/version)
+            og_version=$(git show origin/master:package/version)
             ./package/version.sh bump ${og_version}
           else
             git merge --no-edit --strategy-option=theirs origin/master