Rendering of mjGEOM_LINE respects size[0] (width argument of mjv_makeconnector), denominated in pixels.

- Before this change, line width was hardcoded to 3 pixels and the width argument of mjv_makeConnector was ignored.
- After this change, the width argument is respected and interpreted in units of pixel. The non-standard width unit is ok since lines can only be drawn programmatically.

PiperOrigin-RevId: 516529265
Change-Id: I27bffabba69cde415d2ada67263a887c9240efbf

src/render/render_gl3.c

@@ -390,7 +390,7 @@ static void renderGeom(const mjvGeom* geom, int mode, const float* headpos,
     break;
 
   case mjGEOM_LINE:                           // line
-    glLineWidth(3*con->lineWidth);
+    glLineWidth(size[0]*con->lineWidth);
     lighting = glIsEnabled(GL_LIGHTING);
     glDisable(GL_LIGHTING);
     glBegin(GL_LINES);