chore: CI: do not fetch complete history

leanprover · Jun 13, 2024 · 16cad2b · 16cad2b
1 parent 6d265b4
commit 16cad2b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -304,7 +304,7 @@ jobs:
       # (needs to be after "Install *" to use the right shell)
       - name: CI Merge Checkout
         run: |
-          git fetch origin ${{ github.sha }}
+          git fetch --depth=1 origin ${{ github.sha }}
           git checkout FETCH_HEAD flake.nix flake.lock
         if: github.event_name == 'pull_request'
       # (needs to be after "Checkout" so files don't get overriden)