We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
When embedding doc-gen4 in a VS Code webview and clicking links in an iframe, the webview does not navigate to the given location:
Unsafe attempt to initiate navigation for frame with URL 'https://leanprover-community.github.io/mathlib4_docs/index.html?vscodeBrowserReqId=1718796086963' from frame with URL 'https://leanprover-community.github.io/mathlib4_docs/navbar.html'. The frame attempting navigation is sandboxed, and is therefore disallowed from navigating its ancestors
This probably doesn't occur in the web browser because top windows use a relaxed policy regarding iframe navigation. It does however mean that we cannot properly embed doc-gen4 in the Lean 4 VS Code extension.
The text was updated successfully, but these errors were encountered:
No branches or pull requests
When embedding doc-gen4 in a VS Code webview and clicking links in an iframe, the webview does not navigate to the given location:
This probably doesn't occur in the web browser because top windows use a relaxed policy regarding iframe navigation. It does however mean that we cannot properly embed doc-gen4 in the Lean 4 VS Code extension.
The text was updated successfully, but these errors were encountered: