jflex/jflex-CharSet_java.patch
2007-04-02 20:02:58 +00:00

22 lines
689 B
Diff

--- ./src/JFlex/CharSet.java.orig 2007-04-02 11:03:11.000000000 -0400
+++ ./src/JFlex/CharSet.java 2007-04-02 11:03:47.000000000 -0400
@@ -94,14 +94,14 @@
}
public String toString() {
- CharSetEnumerator enum = characters();
+ CharSetEnumerator enumer = characters();
StringBuffer result = new StringBuffer("{");
- if ( enum.hasMoreElements() ) result.append(""+enum.nextElement());
+ if ( enumer.hasMoreElements() ) result.append(""+enumer.nextElement());
- while ( enum.hasMoreElements() ) {
- int i = enum.nextElement();
+ while ( enumer.hasMoreElements() ) {
+ int i = enumer.nextElement();
result.append( ", "+(int)i);
}