on.save_settings = function()
return {
font_height = Font_height,
foreground_color = Foreground_color,
background_color = Background_color,
deleted_example_panes = Deleted_example_panes,
loaded_filenames = filenames_from_all_panes(),
}
end