}
/* Re-enable color */
gl.glColorMask(true, true, true, true);
gl.glStencilFunc(GL.GL_EQUAL, 1, 1);
gl.glStencilOp(GL.GL_ZERO, GL.GL_ZERO, GL.GL_ZERO);
// push the current color
gl.glPushAttrib(GL2.GL_CURRENT_BIT);
// use the current polygon's color