Open pfitzseb opened 2 years ago
A dark color theme would be very useful. Here is the current display in Pluto/firefox:
It seems to be set in https://github.com/pfitzseb/jl-profile.js/blob/a13f2ef7852bc1782ec180e3efd4ccef2da7ba6d/dist/profile-viewer.js#L291-L301
Workaround for Pluto (changing things only for dark mode): add this cell to the notebook
html""" <style> @media (prefers-color-scheme: dark) { .__profiler-tooltip { background-color: #333; border: 1px solid #777; } } </style> """
I'm not familiar enough with js or css to know whether this is the right thing to do though.
js
css
A dark color theme would be very useful. Here is the current display in Pluto/firefox:
It seems to be set in https://github.com/pfitzseb/jl-profile.js/blob/a13f2ef7852bc1782ec180e3efd4ccef2da7ba6d/dist/profile-viewer.js#L291-L301
Workaround for Pluto (changing things only for dark mode): add this cell to the notebook
I'm not familiar enough with
js
orcss
to know whether this is the right thing to do though.