From 5c7a943719429f18c567e2562f42ca90b999ff35 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 28 Mar 2019 16:50:25 +0100
Subject: [dune] Don't regenerate ltac/dune after bootstrapping.

Once we have the good `plugins/ltac/dune` in place for bootstrapping,
we should not regenerate it. Thanks to @maximedenes for the report.

This fixes `make states` always rebuilding ltac's dependencies.
---
 Makefile.dune | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Makefile.dune b/Makefile.dune
index 4609c563d9..ebf74978a9 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -42,8 +42,10 @@ help:
 	@echo "  - help:    show this message"
 
 # We need to bootstrap with a dummy coq.plugins.ltac so install targets do work.
-voboot:
+plugins/ltac/dune:
 	@echo "(library (name ltac_plugin) (public_name coq.plugins.ltac) (modules_without_implementation extraargs extratactics))" > plugins/ltac/dune
+
+voboot: plugins/ltac/dune
 	dune build $(DUNEOPT) @vodeps
 	dune exec ./tools/coq_dune.exe $(BUILD_CONTEXT)/.vfiles.d
 
-- 
cgit v1.2.3