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

Attached to Project: Community Packages
Opened by Maciej Piechotka (Uzytkownik) - Friday, 29 November 2019, 20:57 GMT
Last edited by Felix Yan (felixonmars) - Friday, 31 July 2020, 07:18 GMT
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 100%
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.
This task depends upon

Closed by  Felix Yan (felixonmars)
Friday, 31 July 2020, 07:18 GMT
Reason for closing:  Fixed
Additional comments about closing:  1.3-2

Loading...