d40c395917
Also: - Increased label width in mjUI tight theme spacing. - Added `mjITEM_EDITFLOAT` for editing float values. - Move mjUI numpad key codes to header file. PiperOrigin-RevId: 535839953 Change-Id: Ibdc0a9a20be514caa5b487211212ed6f5b8a6ba9