public void setMarginHeight(int mh) {
		margin_height = mh;
		repaint();
	}
Sets the margin height
@param mh the new margin height.
Ghidra/Framework/Docking/src/main/java/docking/widgets/MultiLineLabel.java