Join GitHub today
GitHub is home to over 31 million developers working together to host and review code, manage projects, and build software together.Sign up
This branch adds
The second half of the pull-request is a set of
One thing not implemented in the PR is an
That was the case in the past, see 1663fe0.
It's better if tools like opam minimize their their dependencies otherwise we quickly run into bootstrapping issues; this both for the dev tools the dependencies themselves may want to use and sometimes things we don't see but downstream system packagers actually run into.
I made some changes suggested by @rjbou : the
P.S.: and there are