Skip to content

Settings panel#3556

Merged
fonsp merged 15 commits into
mainfrom
settings
May 25, 2026
Merged

Settings panel#3556
fonsp merged 15 commits into
mainfrom
settings

Conversation

@fonsp

@fonsp fonsp commented May 22, 2026

Copy link
Copy Markdown
Member

A new settings panel with a small number of settings. Different people need different things :) I am not intending this to become very big – Pluto is still an opinionated IDE with smart defaults. Just a little bit less now :p

image

New footer:

Scherm­afbeelding 2026-05-22 om 15 53 03

Noteworthy:

TODO

  • Check Tab indent settings

Try this Pull Request!

Open Julia and type:

julia> import Pkg
julia> Pkg.activate(temp=true)
julia> Pkg.add(url="https://github.com/JuliaPluto/Pluto.jl", rev="settings")
julia> using Pluto

@fonsp fonsp added frontend Concerning the HTML editor user request Requested using the feedback form inside Pluto notebooks accessibility Accessibility improvements of the frontend, like screen reader support and internationalization wide audience This affects a wide audience of Pluto users and future Pluto users labels May 22, 2026
@fonsp fonsp changed the title Settings Settings panel May 22, 2026
@fonsp fonsp merged commit 3670f5a into main May 25, 2026
12 of 16 checks passed
@fonsp fonsp deleted the settings branch May 25, 2026 21:30
@fonsp fonsp mentioned this pull request Jun 1, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

accessibility Accessibility improvements of the frontend, like screen reader support and internationalization frontend Concerning the HTML editor user request Requested using the feedback form inside Pluto notebooks wide audience This affects a wide audience of Pluto users and future Pluto users

Projects

None yet

Development

Successfully merging this pull request may close these issues.

tabs/indenting

1 participant