From 7cc152d74039b385b58ff36a580d5dd30af1e81e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?J=C3=A9r=C3=A9mie=20Dimino?= <jeremie@dimino.org>
Date: Sun, 26 Feb 2017 21:40:09 +0000
Subject: [PATCH] Do not install cmdliner

It is only used by the binary, not the library.
---
 vendor/cmdliner/src/jbuild | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/vendor/cmdliner/src/jbuild b/vendor/cmdliner/src/jbuild
index 4c24a5d3..95578953 100644
--- a/vendor/cmdliner/src/jbuild
+++ b/vendor/cmdliner/src/jbuild
@@ -1,6 +1,5 @@
 (jbuild_version 1)
 
 (library
- ((name        jbuilder_cmdliner)
-  (public_name jbuilder.cmdliner)
+ ((name jbuilder_cmdliner)
   (flags (-w -3-6-27-32-33-35-50))))