diff options
| author | Gaëtan Gilbert | 2019-11-08 11:36:22 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-08 11:36:22 +0100 |
| commit | 6930dd3533e7829184daa4cd8a84be62d9886c77 (patch) | |
| tree | 78600ee4e921af2ebaf67dd42e9cb6594f52745c /Makefile.build | |
| parent | 4658804c1f5d9c89f23e2c31a44643ed4569f9fe (diff) | |
coqdep: only output vos when passed -vos
This fixes dune. TBH the problem is that dune is too strict, but we
can't go back in time to change it.
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 b63d582740..ff0e5dbaea 100644 --- a/Makefile.build +++ b/Makefile.build @@ -897,7 +897,7 @@ endif $(VDFILE).d: $(D_DEPEND_BEFORE_SRC) $(VFILES) $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(SHOW)'COQDEP VFILES' - $(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) -Q user-contrib "" $(USERCONTRIBINCLUDES) $(VFILES) $(TOTARGET) + $(HIDE)$(COQDEPBOOT) -vos -boot $(DYNDEP) -Q user-contrib "" $(USERCONTRIBINCLUDES) $(VFILES) $(TOTARGET) ########################################################################### |