I was looking at our /process.sed script and wondered if it's still used.
It is and was added in a0a24fc and 3a98255 to be able to filter out the lib and doc fields from the generated .install file (which are auto-filled by dune for some reason)
However it feels to me that it's a band-aid for an opam-installer feature that seems useful to me: a way to install a package partially.
This would allow us to replace this script by a simple: opam-installer --exclude-sections=doc,lib
I was looking at our
/process.sedscript and wondered if it's still used.It is and was added in a0a24fc and 3a98255 to be able to filter out the
libanddocfields from the generated .install file (which are auto-filled by dune for some reason)However it feels to me that it's a band-aid for an opam-installer feature that seems useful to me: a way to install a package partially.
This would allow us to replace this script by a simple:
opam-installer --exclude-sections=doc,lib