leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: copy code


Johan Commelin (Aug 31 2020 at 13:29):

https://github.com/zulip/zulip/issues/15208 got added to zulip :octopus:

Johan Commelin (Aug 31 2020 at 13:30):

If you hover over a code-block, you'll see a "copy code" icon in the top right.

Reid Barton (Aug 31 2020 at 13:31):

whoa it works

Patrick Massot (Aug 31 2020 at 13:35):

Very nice quality of life little improvement!


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll