Boris Faure a416458ca9 options_theme: ensure the selected theme is the right one ... was not the case when explicitly setting them from command line		2020-11-22 20:42:58 +01:00
..
bin	options_theme: ensure the selected theme is the right one	2020-11-22 20:42:58 +01:00