Closed Seasawher closed 6 months ago
Thanks for the great book!
It would be useful in some cases to add a button to the Lean code block that, when clicked, takes the user to the Lean Web Editor. Just like the jump button on zulip.
If it is OK, I will submit a PR.
Thanks for the great book!
It would be useful in some cases to add a button to the Lean code block that, when clicked, takes the user to the Lean Web Editor. Just like the jump button on zulip.
If it is OK, I will submit a PR.