Idris2
Idris2 copied to clipboard
idris-lang
[ fix ] Fix Makefile targets for `linear` and `papers` libraries
It's on purpose that the papers/ library is not installed with the other ones as it's not meant to be
reusable content but rather propaganda / complex constructions taken from papers.
It's on purpose that the
papers/library is not installed with the other ones as it's not meant to be reusable content but rather propaganda / complex constructions taken from papers.
I removed papers library from install targets. This PR still has other fixes.
FTR, before merging this please consider https://github.com/idris-lang/Idris2/pull/1990 because they will clash with each other.
also, note to self: this possibly has stuff that should/could be incorporated there.
With the closure of #1990, what does the status of this become? Should it still be considered for merging (possibly with some changes), or should it be closed?
Right, with that I think this is good to go. There's a target for linear, which is something we want to let people experiment with, and if people want to be (even more) on the bleeding edge, they can install papers manually.
Thanks for all your efforts ska80! : )