batteries icon indicating copy to clipboard operation
batteries copied to clipboard

chore: adaptations for leanprover/lean4#3756

Open astrainfinita opened this issue 1 year ago • 1 comments

astrainfinita avatar Apr 24 '24 17:04 astrainfinita

Apologies, I needed to reset nightly-testing, and incorrectly deleted it instead. @negiizhao , you may need to reconstitute this PR.

kim-em avatar May 03 '24 03:05 kim-em