--- old/src/demo/share/jfc/Notepad/ElementTreePanel.java 2020-02-22 01:42:31.000000000 -0800 +++ new/src/demo/share/jfc/Notepad/ElementTreePanel.java 2020-02-22 01:42:30.000000000 -0800 @@ -115,7 +115,7 @@ if (as != null) { StringBuilder retBuffer = new StringBuilder("["); - Enumeration names = as.getAttributeNames(); + Enumeration names = as.getAttributeNames(); while (names.hasMoreElements()) { Object nextName = names.nextElement();