Skip to content

fix: url import and decoding not working#104

Merged
joneugster merged 2 commits intomainfrom
fix/url-import
Apr 11, 2026
Merged

fix: url import and decoding not working#104
joneugster merged 2 commits intomainfrom
fix/url-import

Conversation

@joneugster
Copy link
Copy Markdown
Collaborator

@joneugster joneugster commented Apr 11, 2026

  • url args should always be encoded before written to the location hash and decoded when parsed
  • fix import file from URL
  • cleanup atoms slightly and fix some issues with the logic around "importedCode"

Addresses #general > Glimpse of Lean lean4web link broken

@joneugster joneugster added the bug Something isn't working label Apr 11, 2026
@joneugster joneugster changed the title fix: fix url import and encoding fix: url import and decoding not working Apr 11, 2026
@joneugster joneugster merged commit a90843e into main Apr 11, 2026
5 checks passed
@joneugster joneugster deleted the fix/url-import branch April 11, 2026 21:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

bug Something isn't working

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@joneugster