Skip to content

Commit

Permalink
chore: switch from lakefile.lean to lakefile.toml
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Jul 1, 2024
1 parent aa91f04 commit 843c3cf
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions lakefile.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
name = "Qq"
defaultTargets = ["Qq"]

[[lean_lib]]
name = "Qq"

0 comments on commit 843c3cf

Please sign in to comment.