Skip to content

Commit

Permalink
Remove checkdecls step
Browse files Browse the repository at this point in the history
  • Loading branch information
pitmonticone committed Jul 21, 2024
1 parent 454592c commit 6084d87
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions .github/workflows/push.yml
Original file line number Diff line number Diff line change
Expand Up @@ -86,8 +86,8 @@ jobs:
leanblueprint web
cp -r blueprint/web docs/blueprint
- name: Check declarations
run: ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
# - name: Check declarations
# run: ~/.elan/bin/lake exe checkdecls blueprint/lean_decls

- name: Copy documentation to `docs/docs`
run: |
Expand Down

0 comments on commit 6084d87

Please sign in to comment.