You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository was archived by the owner on Oct 25, 2023. It is now read-only.
The web editor's urls do not escape brackets. Brackets are used as part of the Markdown syntax on many popular websites where Lean might be discussed such as StackOverflow, GitHub and Reddit. This means that a Live url posted to such a site might leak out of the containing brackets as shown in this example screenshot.
Workaround is to paste the url into a text editor then search for open brackets and replace them with %28 then search for close brackets and replace them with %29 (so I was able to get my question posted and answered). I suggest it would be preferable if the live editor made these changes to the url automatically.
The web editor's urls do not escape brackets. Brackets are used as part of the Markdown syntax on many popular websites where Lean might be discussed such as StackOverflow, GitHub and Reddit. This means that a Live url posted to such a site might leak out of the containing brackets as shown in this example screenshot.
Workaround is to paste the url into a text editor then search for open brackets and replace them with %28 then search for close brackets and replace them with %29 (so I was able to get my question posted and answered). I suggest it would be preferable if the live editor made these changes to the url automatically.