chore: add dune-workspace file

This commit is contained in:
Simon Cruanes 2023-08-29 14:21:14 -04:00
parent c1b6312cad
commit c4bbec092a
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 7 additions and 0 deletions

View file

@ -12,6 +12,9 @@ test:
doc: doc:
@dune build $(DUNE_OPTS) @doc @dune build $(DUNE_OPTS) @doc
build-dev:
dune build @install @runtest $(DUNE_OPTS) --workspace=dune-workspace.dev
WATCH?= @check @runtest WATCH?= @check @runtest
watch: watch:
dune build $(DUNE_OPTS) -w $(WATCH) dune build $(DUNE_OPTS) -w $(WATCH)

4
dune-workspace.dev Normal file
View file

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