[pacman-dev] [PATCH] makepkg: Add used options to PKGINFO file

[Xavier]

On Thu, Jul 24, 2008 at 2:41 PM, Allan McRae <allan at archlinux.org> wrote:
> Allan McRae wrote:
>> Adds defined options to the PKGINFO file in the form of "makepkgopt =".
>> It may be useful to be able to add these to the pacman DB at some point
>> as that would allow (e.g.) checking which packages have had their docs
>> striped (FS#7092).
>>
>
> This is more of a "might be a good idea" patch being put out there to
> gather opinions.
>

This might be a good idea :)
But apparently known options regroup both BUILDENV and OPTIONS array.
In my opinion, only OPTIONS is interesting.
And then, we might want to just include enabled options, for the sake
of being concise.