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