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

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. Allan