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
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
|
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
Friday, 31 July 2020, 07:18 GMT
Reason for closing: Fixed
Additional comments about closing: 1.3-2