From add9450a5da0d10b1432ce46b5f32c627764fef4 Mon Sep 17 00:00:00 2001 From: Jeremie Dimino Date: Fri, 24 Feb 2017 10:04:40 +0000 Subject: [PATCH] Switch jbuilder to (jbuilder_version 1) --- jbuild | 1 + vendor/cmdliner/src/jbuild | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) create mode 100644 jbuild diff --git a/jbuild b/jbuild new file mode 100644 index 00000000..0947b360 --- /dev/null +++ b/jbuild @@ -0,0 +1 @@ +(jbuilder_version 1) diff --git a/vendor/cmdliner/src/jbuild b/vendor/cmdliner/src/jbuild index 3472cf77..ab3d9c80 100644 --- a/vendor/cmdliner/src/jbuild +++ b/vendor/cmdliner/src/jbuild @@ -1,5 +1,5 @@ (library ((name jbuilder_cmdliner) (public_name jbuilder.cmdliner) - (extra_disabled_warnings (3 6 27 32 33 35 50)) + (flags (-w -3-6-27-32-33-35-50)) (preprocess no_preprocessing)))