Closed unp1 closed 6 months ago
It seems that settings in general are not saved. Changing the appearance or font size also gets lost.
I seem to have found the point where it goes wrong (using the extension example):
ExtensionSettings
are added to ProofIndependentSettings
lastReadedProperties
are read to extract extension settingsAbstractPropertiesSettings#readSettings(Properties)
"disabled"
to get disabled extensionsExtensions > disabled
in the JSON file"disabled"
is found; use defaultI think the JSON file is not properly read and reading it as Properties
seems incorrect. Iirc, @wadoon implemented this. I am not familiar enough to change it.
@Drodt Thanks for looking into it!
I fixed the particular case of not being able to disable extensions in #3392
This is fixed now that #3392 is merged
Description
Deactivating an extension (like Javac, Caching) does not work.
Reproducible
always
Steps to reproduce
Extension is deactivated