2023-11-21 20:11:26 +00:00
|
|
|
on.load_settings = function(settings)
|
|
|
|
Font_height = settings.font_height or font_height
|
|
|
|
Background_color = settings.background_color or Background_color
|
|
|
|
-- careful not to replace the Foreground_color table instance
|
|
|
|
if settings.foreground_color then
|
|
|
|
local src = settings.foreground_color
|
|
|
|
local dest = Foreground_color
|
|
|
|
dest.r, dest.g, dest.b, dest.a = src.r, src.g, src.b, src.a
|
|
|
|
end
|
2023-11-23 05:22:34 +00:00
|
|
|
Deleted_example_panes = settings.deleted_example_panes
|
2023-11-26 20:26:22 +00:00
|
|
|
Initial_load_filenames = settings.loaded_filenames
|
2023-11-21 20:11:26 +00:00
|
|
|
end
|