Add Makefile.

finite-set-exercises
Joshua Potter 2023-05-13 12:28:34 -06:00
parent 11b6e114af
commit f699adb5f6
3 changed files with 8 additions and 19 deletions

7
Makefile Normal file
View File

@ -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

View File

@ -21,7 +21,7 @@ allows generating PDFs and including them in the navbar. To generate
documentation and serve files locally, run the following: documentation and serve files locally, run the following:
```bash ```bash
> lake build Bookshelf:docs > make docs
> lake run server > lake run server
``` ```

View File

@ -77,25 +77,7 @@ target coreDocs : FilePath := do
} }
return (dataFile, trace) 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 library_facet docs (lib) : FilePath := do
run_sh "run_pdflatex"
-- Ordering is important. The index file is generated by walking through the -- Ordering is important. The index file is generated by walking through the
-- filesystem directory. Files copied from the shell scripts need to exist -- filesystem directory. Files copied from the shell scripts need to exist
-- prior to this. -- prior to this.