You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently a .install file needs to be written at the root of the package build directory to be considered.
However the natural location of such a file is rather in the build directory of the build system: this make it easy to clean and need no special line in our .gitignores.
So I think it would be nice to have a field
install-file: <string>
that allows to specify its location w.r.t. to the root of the package build directory (the semantics of the .install file remains however exactly the same, i.e. relative file paths therein are expressed relative to the root of the package build directory).
If something like #3797 becomes a reality end users won't be even bothered to have to write this down as most opam files will end-up being generated anyways.
The text was updated successfully, but these errors were encountered:
Currently a
.install
file needs to be written at the root of the package build directory to be considered.However the natural location of such a file is rather in the build directory of the build system: this make it easy to clean and need no special line in our
.gitignore
s.So I think it would be nice to have a field
that allows to specify its location w.r.t. to the root of the package build directory (the semantics of the
.install
file remains however exactly the same, i.e. relative file paths therein are expressed relative to the root of the package build directory).If something like #3797 becomes a reality end users won't be even bothered to have to write this down as most
opam
files will end-up being generated anyways.The text was updated successfully, but these errors were encountered: