@@ -2738,11 +2738,11 @@ /** * Returns the index of the specified child, or -1 if * <code>child</code> isn't a valid child. */ public int indexOf(ElementInfo child) { - ArrayList children = this.children; + ArrayList<ElementInfo> children = this.children; if (children != null) { return children.indexOf(child); } return -1;