}
super.onMouseUp(mouse);
+
+ if (mouse.isMouse1() && mouseOnVerticalScroller(mouse)) {
+ // Clicked on vertical scrollbar
+ terminal.setVerticalValue(getVerticalValue());
+ }
}
/**
}
super.onMouseMotion(mouse);
+
+ if (mouse.isMouse1() && mouseOnVerticalScroller(mouse)) {
+ // Clicked/dragged on vertical scrollbar
+ terminal.setVerticalValue(getVerticalValue());
+ }
}
// ------------------------------------------------------------------------