From f699adb5f690de8272d0d18b4fca479548f929a3 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Sat, 13 May 2023 12:28:34 -0600
Subject: [PATCH] Add Makefile.

---
 Makefile      |  7 +++++++
 README.md     |  2 +-
 lakefile.lean | 18 ------------------
 3 files changed, 8 insertions(+), 19 deletions(-)
 create mode 100644 Makefile

diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..cc8da16
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,7 @@
+all:
+	@echo "Please specify a build target."
+
+docs:
+	-rm -r build/doc
+	-./scripts/run_pdflatex.sh build > /dev/null
+	lake build Bookshelf:docs
diff --git a/README.md b/README.md
index 96658c7..05fdf34 100644
--- a/README.md
+++ b/README.md
@@ -21,7 +21,7 @@ allows generating PDFs and including them in the navbar. To generate
 documentation and serve files locally, run the following:
 
 ```bash
-> lake build Bookshelf:docs
+> make docs
 > lake run server
 ```
 
diff --git a/lakefile.lean b/lakefile.lean
index 532bd7d..fa08094 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -77,25 +77,7 @@ target coreDocs : FilePath := do
       }
     return (dataFile, trace)
 
-/--
-Wrapper for running scripts found in the `script` directory.
--/
-def run_sh (name : String) : IndexBuildM Unit := do
-  let some bookshelfPkg ← findPackage? `«bookshelf»
-    | error "no bookshelf package found in workspace"
-  let proc <- IO.Process.output {
-    cmd := bookshelfPkg.dir.toString ++ s!"/scripts/{name}.sh",
-    args := #[(← getWorkspace).root.buildDir.toString]
-  }
-  if proc.exitCode == 0 then
-    let out := proc.stdout.trim
-    if out.length > 0 then IO.println out
-  else
-    let err := proc.stderr.trim
-    if err.length > 0 then IO.eprintln err
-
 library_facet docs (lib) : FilePath := do
-  run_sh "run_pdflatex"
   -- Ordering is important. The index file is generated by walking through the
   -- filesystem directory. Files copied from the shell scripts need to exist
   -- prior to this.