idris2-elab-util icon indicating copy to clipboard operation
idris2-elab-util copied to clipboard

Published 20 hours ago • verified publisher icon stefan-hoeck

[ upstream ] Adapt to the changes in idris-lang/Idris2#2517

Open buzden opened this issue 3 years ago • 2 comments

Just in case if idris-lang/Idris2#2517 is accepted

buzden avatar Jun 02 '22 04:06 buzden

Thanks. Can you ping me, once the PR is ready for merging?

stefan-hoeck avatar Jun 02 '22 04:06 stefan-hoeck

Thanks. Can you ping me, once the PR is ready for merging?

Sure!

buzden avatar Jun 02 '22 04:06 buzden