diff options
Diffstat (limited to 'plugins/externaltools')
| -rwxr-xr-x | plugins/externaltools/tools/tools.ui | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/externaltools/tools/tools.ui b/plugins/externaltools/tools/tools.ui index 8b40ad98..fde220d1 100755 --- a/plugins/externaltools/tools/tools.ui +++ b/plugins/externaltools/tools/tools.ui @@ -131,7 +131,6 @@ <property name="default_height">500</property> <property name="type_hint">dialog</property> <property name="skip_taskbar_hint">True</property> - <property name="has_separator">False</property> <signal name="focus_out_event" handler="on_tool_manager_dialog_focus_out"/> <signal name="response" handler="on_tool_manager_dialog_response"/> <child internal-child="vbox"> |