From cd8b8974e2d62a3c3c4d7572921b5a83cbb8642c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 8 Oct 2018 16:09:49 +0200 Subject: [gramlib] Wrap `Gramlib`. This introduces a bit of noise in the Dune files but for now I think it is the best way to do it. --- gramlib/dune | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'gramlib') diff --git a/gramlib/dune b/gramlib/dune index f7605fa9f3..6a9e622b4c 100644 --- a/gramlib/dune +++ b/gramlib/dune @@ -1,4 +1,3 @@ (library (name gramlib) - (public_name coq.gramlib) - (wrapped false)) + (public_name coq.gramlib)) -- cgit v1.2.3