From ed0dc18a0acf752f3bb80f67ee8c7505009e6515 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Mon, 13 Feb 2023 17:09:20 -0700
Subject: [PATCH] Remove `Main.lean`.

---
 Main.lean     | 4 ----
 lakefile.lean | 6 +-----
 2 files changed, 1 insertion(+), 9 deletions(-)
 delete mode 100644 Main.lean

diff --git a/Main.lean b/Main.lean
deleted file mode 100644
index e60cc2b..0000000
--- a/Main.lean
+++ /dev/null
@@ -1,4 +0,0 @@
-import «Bookshelf»
-
-def main : IO Unit :=
-  IO.println s!"Hello, {hello}!"
diff --git a/lakefile.lean b/lakefile.lean
index 86589d0..e91ff6f 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -5,11 +5,7 @@ package «bookshelf» {
   -- add package configuration options here
 }
 
+@[default_target]
 lean_lib «Bookshelf» {
   -- add library configuration options here
 }
-
-@[default_target]
-lean_exe «bookshelf» {
-  root := `Main
-}