Replace make lib-ext
with a configure-based check
#4776
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
make lib-ext
is an artefact from the pre-Jbuilder days when it actually built .cma and .cmxa archives to be put into a separatelib
directory. The workflow has never made sense since the switch to using jbuilder/dune vendored libraries for this.This PR is on buy one, get two free:
--without-dune
is added toconfigure
to allow disabling or forcing the use ofdune
fromPATH
. This is related. Default behaviour is unchanged: if you don't specify anything, Dune will be automatically built if it's missing.--with-vendored-deps
now replacesmake lib-ext
. By default, this gets enabled whenever the oldlib-ext
message would have been disabled. At the end ofconfigure
, sources are downloaded and extracted as required. It's all the same mechanism, it's only invocation which has altered, so full tarballs would use their local copies in the "download" phase, etc.