Fetch the specific branch requested

OffchainLabs · Jul 9, 2024 · 95fb275 · 95fb275
1 parent 4c78892
commit 95fb275
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/.github/workflows/submodule-pin-check.sh b/.github/workflows/submodule-pin-check.sh
@@ -10,8 +10,7 @@ for mod in `git submodule --quiet foreach 'echo $name'`; do
 	branch=origin/HEAD
 	if [[ -v exceptions[$mod] ]]; then
 		branch=${exceptions[$mod]}
-		git -C $mod fetch
-		git -C $mod branch -r
+		git -C $mod fetch `echo $branch | tr "/" " "`
 	fi
 
 	if ! git -C $mod merge-base --is-ancestor HEAD $branch; then