Merge branch 'master' into highprecision

nickbattle · Jan 6, 2024 · 6764185 · 6764185
2 parents 919f7d6 + 68eb7bd
commit 6764185
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/mapper/ClassMapper.java b/vdmj/src/main/java/com/fujitsu/vdmj/mapper/ClassMapper.java
@@ -965,6 +965,11 @@ else if (mp.unmapped)
 	 */
 	private void mark()
 	{
+		if (marked != null)
+		{
+			errorStream.println("WARNING: Nested call to convertLocal?");
+		}
+
 		marked = new Vector<Long>();
 	}