From c4bbec092a88a9752967e9eee2f77755c3450c4b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 29 Aug 2023 14:21:14 -0400 Subject: [PATCH] chore: add dune-workspace file --- Makefile | 3 +++ dune-workspace.dev | 4 ++++ 2 files changed, 7 insertions(+) create mode 100644 dune-workspace.dev diff --git a/Makefile b/Makefile index 16fa5b64..520ee90c 100644 --- a/Makefile +++ b/Makefile @@ -12,6 +12,9 @@ test: doc: @dune build $(DUNE_OPTS) @doc +build-dev: + dune build @install @runtest $(DUNE_OPTS) --workspace=dune-workspace.dev + WATCH?= @check @runtest watch: dune build $(DUNE_OPTS) -w $(WATCH) diff --git a/dune-workspace.dev b/dune-workspace.dev new file mode 100644 index 00000000..0481c82e --- /dev/null +++ b/dune-workspace.dev @@ -0,0 +1,4 @@ +(lang dune 3.0) +;(context (opam (switch 4.08.1))) +(context (opam (switch 4.14.0))) +(context (opam (switch 5.0.0)))