Bugfix: Manchmal wurden nicht alle Marker verschoben.

This commit is contained in:
michael 2020-04-16 18:49:37 +02:00
parent c7fae51dd0
commit 3c469b567b

View File

@ -143,7 +143,7 @@ public class TypeReplaceMarker extends JavMarker implements Comparable {
TypeReplaceMarker other = (TypeReplaceMarker)o; TypeReplaceMarker other = (TypeReplaceMarker)o;
if (this.getPositionInCode() == other.getPositionInCode()) { if (this.getPositionInCode() == other.getPositionInCode()) {
return 0; return this.tip.getInsertString().compareTo(other.tip.getInsertString());
} else if (this.getPositionInCode() > other.getPositionInCode()) { } else if (this.getPositionInCode() > other.getPositionInCode()) {
return 1; return 1;
} else { } else {