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 /dune | |
| 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 'dune')
| -rw-r--r-- | dune | 6 |
1 files changed, 5 insertions, 1 deletions
@@ -25,7 +25,11 @@ (source_tree theories) (source_tree plugins) (source_tree user-contrib)) - (action (with-stdout-to .vfiles.d (bash "%{bin:coqdep} -dyndep both -noglob -boot `find theories plugins user-contrib -type f -name *.v`")))) + (action + (with-stdout-to .vfiles.d + (bash "%{bin:coqdep} -dyndep both -noglob -boot -R theories Coq -R plugins Coq -Q user-contrib/Ltac2 Ltac2 -I user-contrib/Ltac2 \ + `find plugins/ -maxdepth 1 -mindepth 1 -type d -printf '-I %p '` \ + `find theories plugins user-contrib -type f -name *.v`")))) (alias (name vodeps) |
