Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Document #236 under "Known issues" + addresss review comments
The explanation is taken from https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/dune.20and.20parallel.20builds. Also, if this is merged, please replace "jbuilder" by "dune" in the issue title, so that people who click the link aren't too confused. Signed-Off-By: Paolo G. Giarrusso <[email protected]>
- Loading branch information