2020-09-26 12:02:53 +02:00
|
|
|
# Frontend to dune.
|
|
|
|
|
2021-01-01 18:07:06 +01:00
|
|
|
# No implicit rules
|
|
|
|
MAKEFLAGS += --no-builtin-rules
|
|
|
|
.SUFFIXES:
|
|
|
|
|
2024-06-20 15:38:37 +02:00
|
|
|
.PHONY: default build install uninstall test clean
|
2021-01-01 16:39:33 +01:00
|
|
|
|
2024-06-20 15:38:37 +02:00
|
|
|
default: build
|
2020-09-26 12:02:53 +02:00
|
|
|
|
2021-01-01 16:39:33 +01:00
|
|
|
|
2024-06-20 15:38:37 +02:00
|
|
|
build:
|
2024-09-05 14:48:58 +02:00
|
|
|
cd top ; ./install_printers.sh > ./lib/install_printers.ml
|
2020-09-26 12:02:53 +02:00
|
|
|
dune build
|
|
|
|
|
2024-06-20 15:38:37 +02:00
|
|
|
build-prof:
|
|
|
|
top/install_printers.sh > top/lib/install_printers.ml
|
|
|
|
dune build --workspace=dune-workspace.profile
|
|
|
|
|
2020-09-26 12:02:53 +02:00
|
|
|
test:
|
|
|
|
dune runtest -f
|
|
|
|
|
2024-06-20 15:38:37 +02:00
|
|
|
test-prof:
|
|
|
|
dune runtest -f --workspace=dune-workspace.profile
|
|
|
|
|
2020-09-26 12:02:53 +02:00
|
|
|
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
|