This fixes one bug I know of: dragging the mouse atop the settings menu was selecting text in the editor underneath.