From ad34e3a7703d326268bab203864aa84ad3718c2c Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Mon, 29 Mar 2021 11:03:50 +0200
Subject: Fix unknown -vos option for coqdep_boot introduced in PR #11074

---
 Makefile.build | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.build')

diff --git a/Makefile.build b/Makefile.build
index d619fd3c85..cbd4f4efbe 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -893,7 +893,7 @@ PLUGININCLUDES=$(addprefix -I plugins/, $(PLUGINDIRS))
 
 $(VDFILE).d: $(D_DEPEND_BEFORE_SRC) $(VFILES) $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT)
 	$(SHOW)'COQDEP    VFILES'
-	$(HIDE)$(COQDEPBOOT) -vos -boot $(DYNDEP) -R theories Coq -R plugins Coq -Q user-contrib "" $(PLUGININCLUDES) $(USERCONTRIBINCLUDES) $(VFILES) $(TOTARGET)
+	$(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) -R theories Coq -R plugins Coq -Q user-contrib "" $(PLUGININCLUDES) $(USERCONTRIBINCLUDES) $(VFILES) $(TOTARGET)
 
 ###########################################################################
 
-- 
cgit v1.2.3