Skip to content

Conversation

@joneugster
Copy link
Collaborator

@joneugster joneugster commented Dec 27, 2025

  • rename "preferences" to "settings"
  • layout switch with new "auto" state
  • remove project selection from settings: it is available as a quick-select and those not fit into the settings
  • fix: saving setting in local storage broken
  • (internal) use jotai to manage the settings
  • (internal) vertical slice for everything settings-related

Unfortunately, this PR temporarily disables the functionality to provide the settings through the searchParams. This should be addressed by using jotai-location to parse these params and will be addressed in a follow-up.

Fixes: #71
Follow-up: #81

@joneugster joneugster added bug Something isn't working enhancement New feature or request labels Dec 27, 2025
@joneugster joneugster merged commit 5bca4a1 into main Dec 28, 2025
13 of 18 checks passed
@faenuccio
Copy link

I see that you marked #71 as resolved, but preferences/settings are still not saved locally on my firefox. Am I doing something wrong?

@joneugster
Copy link
Collaborator Author

I'm not sure the latest version has been deployed before I went for holidays. Might just be this. Let me reopen and wait to confirm

@joneugster
Copy link
Collaborator Author

Can't reopen from mobile. I'll deploy on the 6th and verify afterwards

@faenuccio
Copy link

Can't reopen from mobile. I'll deploy on the 6th and verify afterwards

Thanks!

@joneugster
Copy link
Collaborator Author

Now deployed to https://lean.math.hhu.de

Will be live on live.lean-lang.org when the FRO bumps their deployment (@nomeata)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bug Something isn't working enhancement New feature or request

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Saving setting in local storage broken.

3 participants