2020-09-26 12:02:53 +02:00
|
|
|
# Frontend to dune.
|
|
|
|
|
|
2021-01-01 16:39:33 +01:00
|
|
|
DIRS=$(shell ls */README.org | sed "s|/README.org||g")
|
|
|
|
|
DOCS=$(patsubst %, docs/%.html, $(DIRS))
|
|
|
|
|
|
2020-09-26 12:02:53 +02:00
|
|
|
.PHONY: default build install uninstall test clean
|
|
|
|
|
|
2021-01-01 17:05:25 +01:00
|
|
|
default: build
|
2021-01-01 16:39:33 +01:00
|
|
|
|
|
|
|
|
|
|
|
|
|
docs/%.html: %/README.org
|
|
|
|
|
- ./bin/tangle.sh $*
|
|
|
|
|
- ./bin/build_doc.sh $*
|
|
|
|
|
|
|
|
|
|
doc: $(DOCS)
|
2020-09-26 12:02:53 +02:00
|
|
|
|
2021-01-01 17:05:25 +01:00
|
|
|
build: doc
|
2020-09-26 12:02:53 +02:00
|
|
|
dune build
|
|
|
|
|
|
|
|
|
|
test:
|
|
|
|
|
dune runtest -f
|
|
|
|
|
|
|
|
|
|
install:
|
|
|
|
|
dune install
|
|
|
|
|
|
|
|
|
|
uninstall:
|
|
|
|
|
dune uninstall
|
|
|
|
|
|
|
|
|
|
clean:
|
|
|
|
|
dune clean
|
|
|
|
|
# Optionally, remove all files/folders ignored by git as defined
|
|
|
|
|
# in .gitignore (-X).
|
|
|
|
|
git clean -dfXq
|
