From f46984bb23ab7402c4cd0c58bd329317c1f94fb3 Mon Sep 17 00:00:00 2001 From: Jeremie Dimino Date: Tue, 24 Apr 2018 15:44:35 +0100 Subject: [PATCH] Add a dune-project file --- dune-project | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 dune-project diff --git a/dune-project b/dune-project new file mode 100644 index 000000000000..fd56c71312bd --- /dev/null +++ b/dune-project @@ -0,0 +1,2 @@ +(lang dune 0.1) +(name dune)