max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: run CI against the head of the branch, not a virtual merge with master (#2769)

Browse source
This commit is contained in:
Scott Morrison 2023-10-27 21:46:49 +11:00 • committed by GitHub
parent dba299ac6a
commit f76a17b33f
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.github/workflows/ci.yml vendored
View file

@ -197,6 +197,8 @@ jobs:
uses: actions/checkout@v3
with:
submodules: true
# the default is to use a virtual merge commit between the PR and master: just use the PR
ref: ${{ github.event.pull_request.head.sha }}
- name: Install Nix
uses: cachix/install-nix-action@v18
with:

3
.github/workflows/nix-ci.yml vendored
View file

@ -34,6 +34,9 @@ jobs:
steps:
- name: Checkout
uses: actions/checkout@v3
with:
# the default is to use a virtual merge commit between the PR and master: just use the PR
ref: ${{ github.event.pull_request.head.sha }}
- name: Install Nix
uses: cachix/install-nix-action@v18
with: