float f = new Float(thresholdValue.getText()).floatValue();
slider.setValue((int) (f * SCALE_FACTOR_1K));
adjustmentValueChanged(null);
+
+ /*
+ * force repaint of any Overview window or structure
+ */
+ changeColour(true);
} catch (NumberFormatException ex)
{
}