| commit | 4fe728df067dc217fcf8a7ad8dc3389e1574b9d4 | [log] [tgz] |
|---|---|---|
| author | Ed Willink <ed@willink.me.uk> | Fri Aug 30 14:40:35 2019 +0100 |
| committer | Ed Willink <ed@willink.me.uk> | Fri Aug 30 14:40:35 2019 +0100 |
| tree | d53778a4a19c3cae3f47c632368e600475c981c1 | |
| parent | e53bb0039fe543a13698fc71e3d393282e050787 [diff] |
[unrelated] Fix UniqueList.clear()
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/UniqueList.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/UniqueList.java index e0ea360..67b012c 100644 --- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/UniqueList.java +++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/UniqueList.java
@@ -104,6 +104,7 @@ @Override public void clear() { + super.clear(); set = null; }