From 69da6e92961d5c7007e7836c2770f9c4a3b9e0e2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 2 Oct 2018 18:23:32 +0200
Subject: [dune] Fix couple of minor bugs in #8617

I forgot to update `.PHONY` and to put the proper flags in the new
workspace file.
---
 dev/dune-workspace.all | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
index 44857ed050..1a8a816aaa 100644
--- a/dev/dune-workspace.all
+++ b/dev/dune-workspace.all
@@ -2,7 +2,7 @@
 
 ; Add custom flags here. Default developer profile is `dev`
 (env
- (dev     (flags :standard -rectypes -w -9-27-50))
+ (dev     (flags :standard -rectypes -w -9-27-50+60))
  (release (flags :standard -rectypes)))
 
 (context (opam (switch 4.05.0)))
-- 
cgit v1.2.3