Skip to content

Commit 75fcd59

Browse files
slashbadeslashbade
committed
fix: remove Main.lean for build err
1 parent f9e8e46 commit 75fcd59

2 files changed

Lines changed: 0 additions & 7 deletions

File tree

‎Main.lean‎

Lines changed: 0 additions & 4 deletions
This file was deleted.

‎lakefile.toml‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,3 @@ defaultTargets = ["requests"]
55
[[lean_lib]]
66
name = "Requests"
77

8-
[[lean_exe]]
9-
name = "requests"
10-
root = "Main"

0 commit comments

Comments
 (0)