Merge pull request #251 from wpferguson/fix_script_manager_scrolling

Make script manager scrollable.
This commit is contained in:
wpferguson
2020-05-23 17:01:52 -04:00
committed by GitHub

View File

@@ -747,7 +747,7 @@ dt.register_lib(
"script manager", -- Visible name
true, -- expandable
false, -- resetable
{[dt.gui.views.lighttable] = {"DT_UI_CONTAINER_PANEL_LEFT_BOTTOM", 100}}, -- containers
{[dt.gui.views.lighttable] = {"DT_UI_CONTAINER_PANEL_LEFT_CENTER", 0}}, -- containers
dt.new_widget("box") -- widget
{
orientation = "vertical",