|
@@ -807,6 +807,7 @@ void TerminalWidget::mousedown_event(GUI::MouseEvent& event)
|
|
else if (m_rectangle_selection)
|
|
else if (m_rectangle_selection)
|
|
m_rectangle_selection = false;
|
|
m_rectangle_selection = false;
|
|
|
|
|
|
|
|
+ m_triple_click_timer.reset();
|
|
update_copy_action();
|
|
update_copy_action();
|
|
update();
|
|
update();
|
|
}
|
|
}
|