From 48831496281521b31618e06512367668d69fd268 Mon Sep 17 00:00:00 2001 From: Marc Lasson Date: Mon, 10 Dec 2018 15:46:08 +0100 Subject: [PATCH] workspace.dev --- dune-workspace.dev | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 dune-workspace.dev diff --git a/dune-workspace.dev b/dune-workspace.dev new file mode 100644 index 0000000..9a02cb0 --- /dev/null +++ b/dune-workspace.dev @@ -0,0 +1,5 @@ +(lang dune 1.2) +(context (opam (switch 4.02.2))) +(context (opam (switch 4.03.0))) +(context (opam (switch 4.04.0))) +(context (opam (switch default)))