Skip to content
New issue

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

Display.published_to_js (v2) #11

Merged
merged 10 commits into from
Jul 17, 2023
Merged

Conversation

disberd
Copy link
Member

@disberd disberd commented Jul 16, 2023

This resurrects #8 and for the moment simply adds some Docstirng to explain document caching.

The other two missing points from the checklist in #8 have been deemed non-necessary for the time being (approved by @fonsp).

If one wants to exploit published_to_js outside of Pluto they must create their own if-else statement in the custom show method checking whether the show is being run inside Pluto or not (using is_inside_pluto).

@fonsp fonsp mentioned this pull request Jul 17, 2023
7 tasks
@fonsp fonsp merged commit 3c94e70 into JuliaPluto:main Jul 17, 2023
@fonsp fonsp linked an issue Nov 21, 2023 that may be closed by this pull request
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Add publish_to_js
2 participants