FS#64685 - [agda-stdlib] should not install Everything.agda
Attached to Project:
Community Packages
Opened by Maciej Piechotka (Uzytkownik) - Friday, 29 November 2019, 20:55 GMT
Last edited by Felix Yan (felixonmars) - Friday, 31 July 2020, 07:18 GMT
Opened by Maciej Piechotka (Uzytkownik) - Friday, 29 November 2019, 20:55 GMT
Last edited by Felix Yan (felixonmars) - Friday, 31 July 2020, 07:18 GMT
|
Details
As far as I know agda-stdlib should not copy Everything.agda
as it may (and do) clash with other libraries.
Removing `Everything.agda*` from cp line should be sufficient |
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