directory rename

Seasawher · Dec 7, 2024 · 82ed498 · 82ed498
1 parent 0e7220c
commit 82ed498
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 4 deletions.
diff --git a/Src/HowToUse.lean → LeanBook/HowToUse.lean b/Src/HowToUse.lean → LeanBook/HowToUse.lean
diff --git a/Src/README.lean → LeanBook/README.lean b/Src/README.lean → LeanBook/README.lean
diff --git a/assets/filePlay.js b/assets/filePlay.js
@@ -8,7 +8,7 @@ function filePlay() {
   playButtonLink.href = playButtonLink.href.replace(/\.md$/, ".lean");
   playButtonLink.href = playButtonLink.href.replace(
     "/booksrc/",
-    "/Src/",
+    "/LeanBook/",
   );
   fetch(playButtonLink.href)
     .then((response) => response.text())

diff --git a/lakefile.lean b/lakefile.lean
@@ -9,8 +9,8 @@ package «Lean Book» where
   ]
 
 @[default_target]
-lean_lib «Src» where
-  globs := #[.submodules `Src] -- Build all files in the `Src` directory.
+lean_lib «LeanBook» where
+  globs := #[.submodules `LeanBook] -- Build all files in the `LeanBook` directory.
 
 require mdgen from git
   "https://github.com/Seasawher/mdgen" @ "main"
@@ -26,6 +26,6 @@ def runCmd (cmd : String) (args : Array String) : ScriptM Bool := do
   return hasError
 
 script build do
-  if ← runCmd "lake" #["exe", "mdgen", "Src", "booksrc"] then return 1
+  if ← runCmd "lake" #["exe", "mdgen", "LeanBook", "booksrc"] then return 1
   if ← runCmd "mdbook" #["build"] then return 1
   return 0