Skip to content

Commit

Permalink
Update push.yml
Browse files Browse the repository at this point in the history
test
  • Loading branch information
CBirkbeck authored Jul 23, 2024
1 parent 36b9220 commit bad4bad
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion .github/workflows/push.yml
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ jobs:
run: ~/.elan/bin/lake -Kenv=dev exe cache get

- name: Build project
run: ~/.elan/bin/lake -Kenv=dev build FltRegular
run: ~/.elan/bin/lake -R -Kenv=dev build FltRegular

- uses: actions/cache@v3
name: Mathlib doc Cache
Expand Down

0 comments on commit bad4bad

Please sign in to comment.