Skip to content

Commit

Permalink
check-friends: pulse uses normal F* package now
Browse files Browse the repository at this point in the history
  • Loading branch information
mtzguido committed Jan 7, 2025
1 parent 99d999c commit b144059
Showing 1 changed file with 8 additions and 8 deletions.
16 changes: 8 additions & 8 deletions .github/workflows/check-friends.yml
Original file line number Diff line number Diff line change
Expand Up @@ -151,11 +151,11 @@ jobs:
repository: mtzguido/pulse
ref: dev

# Since pulse needs F* internal build files, we can't use
# binary nor source packages. So we get the whole repo.
- uses: mtzguido/gci-download@master
- uses: actions/download-artifact@v4
with:
name: fstar-repo
name: fstar.tar.gz
- run: tar -xzf fstar.tar.gz
- run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV

- name: Build (after setting up cargo env)
run: . $HOME/.cargo/env && make -C pulse -skj$(nproc)
Expand All @@ -177,11 +177,11 @@ jobs:
- run: echo "HOME=/home/user" >> $GITHUB_ENV
- uses: mtzguido/set-opam-env@master

# Since pulse needs F* internal build files, we can't use
# binary nor source packages. So we get the whole repo.
- uses: mtzguido/gci-download@master
- uses: actions/download-artifact@v4
with:
name: fstar-repo
name: fstar.tar.gz
- run: tar -xzf fstar.tar.gz
- run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV

- uses: mtzguido/gci-download@master
with:
Expand Down

0 comments on commit b144059

Please sign in to comment.