mirror of
https://github.com/zyedidia/micro.git
synced 2026-02-06 07:00:24 +09:00
Passing options via micro -option=value in the command line should only temporarily override the option value for the current micro session, not change it permanently in settings.json. But currently it wrongly writes it to settings.json in the case when the value passed via command line is the default value of this option, while the current permanent setting in settings.json is a non-default value. Fixes #3005