Idris2 icon indicating copy to clipboard operation
Idris2 copied to clipboard

Published 20 hours ago • verified publisher icon idris-lang

Update INSTALL.md

Open buggymcbugfix opened this issue 1 year ago • 3 comments

To successfully build Idris2 and run the tests, I had to set some environment variables, see also this discussion on Discord.

For the benefit of others, I think it makes sense to add this to the Installation instructions.

buggymcbugfix avatar Oct 09 '22 00:10 buggymcbugfix

Hi there, can you replace your link to discord with a summary of the situation? People on Github might not have access to discord, and it makes it easier to review if all the information necessary is on the PR description wihtout having to follow any links.

Thanks!

andrevidela avatar Oct 09 '22 09:10 andrevidela

Related: #2233 might already be addressed by: #2669 ?

CodingCellist avatar Oct 10 '22 07:10 CodingCellist

I merely documented what worked for me. Feel free to close/amend this PR.

buggymcbugfix avatar Oct 11 '22 09:10 buggymcbugfix

... might already be addressed by: #2669 ?

probably not. I don't think I edit any installation instructions in that, just move them about

joelberkeley avatar Oct 27 '22 18:10 joelberkeley