From e9b37e0c747b2e5e9a5701297de026e2b7faacf9 Mon Sep 17 00:00:00 2001 From: Kate Date: Fri, 10 Jan 2020 12:56:03 +0000 Subject: [PATCH] Remove unused dune extension --- dune-project | 1 - 1 file changed, 1 deletion(-) diff --git a/dune-project b/dune-project index 4da0e2863..eef99a8b3 100644 --- a/dune-project +++ b/dune-project @@ -1,3 +1,2 @@ (lang dune 1.2) (name dns) -(using menhir 2.0)