Skip to content

Conversation

@rjbou
Copy link
Collaborator

@rjbou rjbou commented Oct 28, 2025

Fixes #6759

@rjbou rjbou added the PR: WIP Not for merge at this stage label Oct 28, 2025
@kit-ty-kate
Copy link
Member

The manual says:

bin: installs to <prefix>/bin/, [...]

adding the option breaks this invariant. While other options such as --mandir, --libdir, etc. already exist and have similar manual entry, i think it would be nice to at least document this a bit more fully, to encompass opam-installer

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

PR: NEEDS UPDATE PR: WIP Not for merge at this stage

Projects

None yet

Development

Successfully merging this pull request may close these issues.

./configure --bindir option is not respected

2 participants