chore: reorganize nascent user's guide

leanprover · Dec 13, 2023 · f8957c8 · f8957c8
1 parent 407c3bb
commit f8957c8
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 3 deletions.
diff --git a/UsersGuide.lean → UsersGuideMain.lean b/UsersGuide.lean → 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
@@ -0,0 +1,5 @@
+import LeanDoc.Genre.Manual
+
+import UsersGuide.Basic
+
+
diff --git a/UsersGuide/Basic.Lean → doc/UsersGuide/Basic.Lean b/UsersGuide/Basic.Lean → doc/UsersGuide/Basic.Lean
diff --git 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.
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,5 @@
		import LeanDoc.Genre.Manual

		import UsersGuide.Basic