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.