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 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Makefile.dune')

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
 
-- 
cgit v1.2.3