Skip to content

Commit

Permalink
change to lakefile
Browse files Browse the repository at this point in the history
  • Loading branch information
@joneugster
joneugster committed Feb 13, 2025
1 parent ec496d2 commit 39a2e44
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion lakefile.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@ import Lake

open Lake DSL


/-!
## Mathlib dependencies on upstream projects
-/
Expand Down

0 comments on commit 39a2e44

Please sign in to comment.