From f8957c848ac160abd448644076c17c5220955ac8 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Wed, 13 Dec 2023 18:07:08 +0100
Subject: [PATCH] chore: reorganize nascent user's guide

---
 UsersGuide.lean => UsersGuideMain.lean    | 3 +--
 doc/UsersGuide.lean                       | 5 +++++
 {UsersGuide => doc/UsersGuide}/Basic.Lean | 0
 lakefile.lean                             | 3 ++-
 4 files changed, 8 insertions(+), 3 deletions(-)
 rename UsersGuide.lean => UsersGuideMain.lean (80%)
 create mode 100644 doc/UsersGuide.lean
 rename {UsersGuide => doc/UsersGuide}/Basic.Lean (100%)

diff --git a/UsersGuide.lean b/UsersGuideMain.lean
similarity index 80%
rename from UsersGuide.lean
rename to UsersGuideMain.lean
index 08e8999..6b3d2e6 100644
--- a/UsersGuide.lean
+++ b/UsersGuideMain.lean
@@ -1,7 +1,6 @@
 import LeanDoc.Genre.Manual
 
-import UsersGuide.Basic
-
+import UsersGuide
 
 open LeanDoc.Genre.Manual
 
diff --git a/doc/UsersGuide.lean b/doc/UsersGuide.lean
new file mode 100644
index 0000000..a13de44
--- /dev/null
+++ b/doc/UsersGuide.lean
@@ -0,0 +1,5 @@
+import LeanDoc.Genre.Manual
+
+import UsersGuide.Basic
+
+
diff --git a/UsersGuide/Basic.Lean b/doc/UsersGuide/Basic.Lean
similarity index 100%
rename from UsersGuide/Basic.Lean
rename to doc/UsersGuide/Basic.Lean
diff --git a/lakefile.lean b/lakefile.lean
index b0418a9..2148707 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -28,10 +28,11 @@ lean_exe «leandoc» where
   supportInterpreter := true
 
 lean_lib UsersGuide where
+  srcDir := "doc"
 
 @[default_target]
 lean_exe usersguide where
-  root := `UsersGuide
+  root := `UsersGuideMain
   -- Enables the use of the Lean interpreter by the executable (e.g.,
   -- `runFrontend`) at the expense of increased binary size on Linux.
   -- Remove this line if you do not need such functionality.