Remove `Main.lean`.
parent
d06097a608
commit
ed0dc18a0a
|
@ -1,4 +0,0 @@
|
||||||
import «Bookshelf»
|
|
||||||
|
|
||||||
def main : IO Unit :=
|
|
||||||
IO.println s!"Hello, {hello}!"
|
|
|
@ -5,11 +5,7 @@ package «bookshelf» {
|
||||||
-- add package configuration options here
|
-- add package configuration options here
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@[default_target]
|
||||||
lean_lib «Bookshelf» {
|
lean_lib «Bookshelf» {
|
||||||
-- add library configuration options here
|
-- add library configuration options here
|
||||||
}
|
}
|
||||||
|
|
||||||
@[default_target]
|
|
||||||
lean_exe «bookshelf» {
|
|
||||||
root := `Main
|
|
||||||
}
|
|
||||||
|
|
Loading…
Reference in New Issue