Skip to content

Commit 066d81d

Browse files
authored
Change dashlist to widthlist in DrawData::getWidth (#39)
1 parent 4bc5e62 commit 066d81d

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

src/main/java/wprover/DrawData.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -96,9 +96,9 @@ public static int getWidthCounter() {
9696
public static double getWidth(int index) {
9797
double d;
9898
try {
99-
d = (double) dd.dashlist.get(index);
99+
d = (double) dd.widthlist.get(index);
100100
} catch (ClassCastException cce) {
101-
d = (int) dd.dashlist.get(index);
101+
d = (int) dd.widthlist.get(index);
102102
}
103103
return d;
104104
}

0 commit comments

Comments
 (0)