agda-mugen icon indicating copy to clipboard operation
agda-mugen copied to clipboard
verified publisher icon RedPRL

Webpage Generation

Open TOTBWF opened this issue 3 years ago • 3 comments

Closes #3

TOTBWF avatar Oct 05 '22 18:10 TOTBWF

So the 1lab uses --no-load-primitives, but there's an agda bug where it tries to get the primitive dir here, and crashes. This is blocked on that bug.

TOTBWF avatar Oct 05 '22 19:10 TOTBWF

Should be fixed in https://github.com/agda/agda/pull/6161

TOTBWF avatar Oct 05 '22 19:10 TOTBWF

What's the current status of this PR?

favonia avatar Jan 01 '23 03:01 favonia

Closed due to lack of progress.

favonia avatar Jun 09 '24 19:06 favonia