From ef4dd8a9ccfaa455622afc97a509a4174a09f6f2 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 4 Mar 2025 22:37:27 -0800
Subject: [PATCH] Don't die on missing fetch

---
 .github/workflows/coq-timing-diff.yml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/coq-timing-diff.yml b/.github/workflows/coq-timing-diff.yml
index 47a05cd334..75fa3c4015 100644
--- a/.github/workflows/coq-timing-diff.yml
+++ b/.github/workflows/coq-timing-diff.yml
@@ -70,8 +70,10 @@ jobs:
         if [[ -n "${{ github.event.inputs.target_repository }}" && "${{ github.event.inputs.target_repository }}" != "${{ github.repository }}" ]]; then
           echo "Adding remote for target repository: ${{ github.event.inputs.target_repository }}"
           git remote add target_repo "https://github.com/${{ github.event.inputs.target_repository }}.git"
+          git fetch target_repo $CURRENT_BRANCH || true
           git checkout -b $CURRENT_BRANCH target_repo/$CURRENT_BRANCH
         else
+          git fetch origin $CURRENT_BRANCH || true
           git checkout -b $CURRENT_BRANCH origin/$CURRENT_BRANCH
         fi
         if [[ -n "$PR_NUMBER" ]]; then
@@ -79,13 +81,13 @@ jobs:
           BASE_BRANCH=$(gh pr view $PR_NUMBER --json baseRefName --jq '.baseRefName')
           echo "This branch has PR #$PR_NUMBER from $CURRENT_BRANCH to $BASE_BRANCH"
           # Get the merge-base of the base branch and current commit
-          git fetch origin $BASE_BRANCH
+          git fetch origin $BASE_BRANCH || true
           BASE_SHA=$(git merge-base target_repo/$BASE_BRANCH $CURRENT_BRANCH)
 
         else
           # For non-PRs, use merge-base of current branch and master as base_sha
           echo "This is not a PR, using merge-base with master"
-          git fetch origin master
+          git fetch origin master || true
           BASE_SHA=$(git merge-base master $CURRENT_BRANCH)
         fi