All ProjectsArch LinuxCommunity PackagesPacmanRelease Engineering Switch

Show Task #

Please read this before reporting a bug:
https://wiki.archlinux.org/title/Bug_reporting_guidelines

Do NOT report bugs when a package is just outdated, or it is in the AUR. Use the 'flag out of date' link on the package page, or the Mailing List.

REPEAT: Do NOT report bugs for outdated packages!

Tasklist

FS#64686 - [agda-stdlib] builds HTML but does not ship it

Task Type Bug Report Category Packages Status Closed Assigned To Felix Yan (felixonmars) Architecture All Severity Low Priority Normal Reported Version Due in Version Undecided Due Date Undecided Percent Complete Votes 0 Private No

Details This is more of optimization of building of package - agda-stdlib builds HTML build it does not copy the files so it should be possible to delete `agda --html -i. -isrc README.agda` without affecting the output.