From a10b7dc5b57a455c989814a5735766b1a9cf79f9 Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Tue, 15 Jan 2019 10:47:57 +0100 Subject: [PATCH] ocplib-json-typed: Makefile update for dune We don't care as we're not using the Makefile directly but: dune: --dev is no longer accepted as it is now the default. --- vendors/ocplib-json-typed/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vendors/ocplib-json-typed/Makefile b/vendors/ocplib-json-typed/Makefile index 4cfc21d4e..d56625796 100644 --- a/vendors/ocplib-json-typed/Makefile +++ b/vendors/ocplib-json-typed/Makefile @@ -1,5 +1,5 @@ all: - dune build @install @runtest --dev + dune build @install @runtest install: dune install