Automate build with Makefile.

2023-05-09 16:21:17 -06:00 · 2023-05-09 16:21:17 -06:00 · a0dd143868
parent f83bd7f0eb
commit a0dd143868
1 changed files with 7 additions and 0 deletions
--- a/7
+++ b/7
@ -0,0 +1,7 @@
+all:
+	@echo "You must specify a specific build task."
+
+bookshelf:
+	-rm -r {lean,_bookshelf/build/doc}
+	(cd _bookshelf && lake build Bookshelf:docs)
+	cp -r _bookshelf/build/doc lean