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.
---
 Makefile.dune          | 8 ++++----
 dev/dune-workspace.all | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Makefile.dune b/Makefile.dune
index ac5f584b90..6733c485fa 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -1,7 +1,7 @@
 # -*- mode: makefile -*-
 # Dune Makefile for Coq
 
-.PHONY: help voboot states world watch release apidoc clean
+.PHONY: voboot states world watch release apidoc ocheck clean help
 
 # use DUNEOPT=--display=short for a more verbose build
 # DUNEOPT=--display=short
@@ -29,9 +29,6 @@ states: voboot
 world: voboot
 	dune build $(DUNEOPT) @install
 
-ocheck: voboot
-	dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all
-
 watch: voboot
 	dune build $(DUNEOPT) @install -w
 
@@ -41,6 +38,9 @@ release: voboot
 apidoc: voboot
 	dune build $(DUNEOPT) @doc
 
+ocheck: voboot
+	dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all
+
 clean:
 	dune clean
 
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