diff options
| author | Emilio Jesus Gallego Arias | 2020-02-05 14:52:03 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-07 13:24:55 +0100 |
| commit | c3775de04c863c644ecfedffa23ddb17f99f2918 (patch) | |
| tree | ef25a343a4467c73dddd179c1b82567b902f05c7 /Makefile.build | |
| parent | 9276876d66defa40adf0ff609c97150a6fe98d58 (diff) | |
[coqdep] Don't treat stdlib specially in boot mode.
This means the build system should pass the correct includes and
library bindings to `coqdep`.
We still have some discrepancies we won't be able to solve until
`Loadpath` and `coqdep` are fused [which depends on the dune build.
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index 814305a2fe..3c32e5bcc2 100644 --- a/Makefile.build +++ b/Makefile.build @@ -865,9 +865,11 @@ endif # Dependencies of .v files +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) -Q user-contrib "" $(USERCONTRIBINCLUDES) $(VFILES) $(TOTARGET) + $(HIDE)$(COQDEPBOOT) -vos -boot $(DYNDEP) -R theories Coq -R plugins Coq -Q user-contrib "" $(PLUGININCLUDES) $(USERCONTRIBINCLUDES) $(VFILES) $(TOTARGET) ########################################################################### |