portal 2025-04-24

I would like to customize my portal font family and size.. I can't find anything in the docs regarding this. And searching this channel reveals portal.api/set-theme but that doesn't seem to exist in the latest portal version. Any tips here? (I'm aware I can change the default monospace font on my system, but I'd like to have a portal specific tweak)

could the messages have been referring to the UI command? that certainly exists in the latest version, I think:

no, this was in reference to the backend.. see https://clojurians.slack.com/archives/C0185BFLLSE/p1697819550003129?thread_ts=1697817436.467999&cid=C0185BFLLSE reading that thread in its entirety, I think that might have been a proposed interface that wasn't ever implemented.

currently still no easy way to do so, but I'd like to add it soon. Do you have any feedback on how you would like to customize this?