chore: merge-checkout test fixed and removed from exclusions on master
This commit is contained in:
parent
121ce56506
commit
3feb63231e
1 changed files with 1 additions and 1 deletions
2
.github/workflows/build-template.yml
vendored
2
.github/workflows/build-template.yml
vendored
|
|
@ -82,7 +82,7 @@ jobs:
|
|||
- name: CI Merge Checkout
|
||||
run: |
|
||||
git fetch --depth=1 origin ${{ github.sha }}
|
||||
git checkout FETCH_HEAD flake.nix flake.lock script/prepare-*
|
||||
git checkout FETCH_HEAD flake.nix flake.lock script/prepare-* tests/lean/run/importStructure.lean
|
||||
if: github.event_name == 'pull_request'
|
||||
# (needs to be after "Checkout" so files don't get overridden)
|
||||
- name: Setup emsdk
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue