Ludovic Courtès <l...@gnu.org> writes: > Efraim Flashner <efr...@flashner.co.il> skribis: > >> On Thu, 25 Feb 2016 21:32:22 +0100 >> Ricardo Wurmus <rek...@elephly.net> wrote: >> >>> Hi Guix, >>> >>> should we install headers to separate outputs as we do it in some cases >>> for really large documentation? It seems wrong to me to download >>> substitutes for libraries when at build time only certain headers are >>> needed. >>> >>> Other distributions have separate “*-devel” or “*-dev” packages (and I’m >>> ambivalent about this) — would it be a bad idea if we provided “devel” >>> or “dev” *outputs* so that users had more control over what ends up in >>> their store? >>> >>> I’m not writing this because I’m annoyed by the current behaviour — I’m >>> just curious. >>> >>> ~~ Ricardo >> >> I thought a bit about it before and I don't really think it'll save that much >> space. Most of the time the headers are a small part of the total package, >> and the fine-tuning that comes with chosing exactly which outputs from a >> build process you actually want seem like they should be left as >> encouragement for people to hack their systems. > > Seconded. We can add a separate “include” output (there’s already a > special case for that in gnu-build-system) on a case-by-case basis, like > we do for documentation, but in practice, I’ve never seen a case where > moving headers away would be a significant space saving.
Thank you all for your comments. I agree that it makes sense to do this on a case-by-case basis only. Curiosity: satisfied :) ~~ Ricardo
