Skip to content

Commit

Permalink
Mathlib 由来の警告があるので、警告があったらエラーにするのを一時的にやめる
Browse files Browse the repository at this point in the history
  • Loading branch information
Seasawher committed Oct 15, 2024
1 parent 79f6818 commit 47033d4
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ jobs:
- name: lean action
uses: leanprover/lean-action@v1
with:
build-args: "--fail-level=warning"
build-args: "--log-level=error"

# Lean の更新により Windows 環境でだけビルドが壊れる可能性もあるので、
# 念のために Windows 環境でもビルドを行う
Expand Down

0 comments on commit 47033d4

Please sign in to comment.