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 has been 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 text was updated successfully, but these errors were encountered:
Antony74
added a commit
to Antony74/lean-web-editor
that referenced
this issue
Feb 18, 2018
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 text was updated successfully, but these errors were encountered: