A while ago I did ask why we do have this thing. The answer was that some tasks (eg refman) was not built by dune directly.
Now the question is: why does this makefile call dune sub-targets instead of just building everything, and then use the installed Coq to do stuff?
What do you mean by "call dune sub-target"
Anyways I wouldn't worry too much, likely tomorrow I'll push the PR that removes these files in full actually
If you have time for the build system, please release dune 2.9.2 and unblock 15220.
Last updated: Nov 29 2023 at 05:01 UTC