Idris2
Idris2 copied to clipboard
translate bootstrap-stage2.sh to bootstrap-stage2.mk
This a attempt to fix https://github.com/idris-lang/Idris2/issues/2152
FTR, there's a PR that completely rewrites how bootstrap is done.
please consider https://github.com/idris-lang/Idris2/pull/1990 when deciding about merging.
FTR, there's a PR that completely rewrites how bootstrap is done.
please consider #1990 when deciding about merging.
that indeed might be better, but lets keep this one open til that one is merged
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?
Given that this was labelled abandoned ~2 months ago and no work or complaints have arisen, including during the IDM in early December 2022, I'm closing this. If it is still relevant, please make the required changes before reopening.