Skip to content

Commit 8920dcb

Browse files
authored
chore: remove unneeded experimental.module option (#123)
1 parent 523ec6f commit 8920dcb

File tree

1 file changed

+0
-3
lines changed

1 file changed

+0
-3
lines changed

lakefile.toml

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,6 @@ name = "Qq"
22
testDriver = "QqTest"
33
defaultTargets = ["Qq"]
44

5-
[leanOptions]
6-
experimental.module = true
7-
85
[[lean_lib]]
96
name = "Qq"
107

0 commit comments

Comments
 (0)