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