lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

feat: lake: build monitor improvements

Open tydeu opened this issue 3 months ago • 1 comments

WIP. Currently implements the polling of finished jobs. Still need to implement printing build captions only when a job actually does something. Also needs integrating with the other refactor touchups.

tydeu avatar May 10 '24 21:05 tydeu