Nicolás Ojeda Bär
Nicolás Ojeda Bär
> I was thinking of something a little simpler, perhaps: Alternatively, a `(dirs)` or `(files)` stanza could be accepted in `dune-project` and/or `dune-workspace` to set default rules.
> 2\. Could someone who is more familiar with Dune development, for whom the addition of new stuff in `dune-project` is easy work, do the work of tweaking the PR...
> > 2. Could someone who is more familiar with Dune development, for whom the addition of new stuff in `dune-project` is easy work, do the work of tweaking the...
Friendly ping. @xvw @bbatsov have you been able to take a look? This PR looked quite promising. It would be great if it could be pushed forward.
> Thanks for looking over those commits, @nojb! I've marked the PR as draft just while the commit from #13728 remains Up to you, but note that strictly speaking you...
Anything left to do here before merging? The PR already has two approvals.
> I don't particularly care if we have more than one name, but I'm strongly against making breaking changes that offer no benefits to the user. So even if we...
Thanks for the fix @garrigue!
> The post-install message could also advise to install ocp-index. This would prevent an error later raised: > > > Error: Completion and doc lookup needs ocp-index. Try 'opam install...
Thanks for the PR! Have you made any benchmarks to have an idea of what is the performance impact of this change? > It would be great if this PR...