diff options
| author | Hendrik Tews | 2021-03-29 11:03:50 +0200 |
|---|---|---|
| committer | Hendrik Tews | 2021-04-12 20:56:40 +0200 |
| commit | ad34e3a7703d326268bab203864aa84ad3718c2c (patch) | |
| tree | ab2fdc8d9ff49b5da8c2ea4f22d7ddc8367fce9f /Makefile.build | |
| parent | 1947e54a2331dbbb8cd0f46b40bbb1524a67df54 (diff) | |
Fix unknown -vos option for coqdep_boot introduced in PR #11074
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
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) ########################################################################### |