Idris2 icon indicating copy to clipboard operation
Idris2 copied to clipboard

translate bootstrap-stage2.sh to bootstrap-stage2.mk

Open xgqt opened this issue 4 years ago • 4 comments

Signed-off-by: Maciej Barć [email protected]

xgqt avatar Nov 25 '21 23:11 xgqt

This a attempt to fix https://github.com/idris-lang/Idris2/issues/2152

xgqt avatar Nov 25 '21 23:11 xgqt

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.

attila-lendvai avatar Dec 03 '21 13:12 attila-lendvai

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

xgqt avatar Dec 03 '21 14:12 xgqt

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?

CodingCellist avatar Oct 03 '22 09:10 CodingCellist

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.

CodingCellist avatar Jan 09 '23 08:01 CodingCellist