diff --git a/org.eventb.texttools/src/org/eventb/texttools/PersistenceHelper.java b/org.eventb.texttools/src/org/eventb/texttools/PersistenceHelper.java index a5b819d3407ec5a394441ec114c098c803f0edb8..4617d4a2356e3558cf7643afcd9504398c1222e8 100644 --- a/org.eventb.texttools/src/org/eventb/texttools/PersistenceHelper.java +++ b/org.eventb.texttools/src/org/eventb/texttools/PersistenceHelper.java @@ -167,8 +167,8 @@ public class PersistenceHelper { try { if (d.getState() != DifferenceState.MERGED) evbMerger.copyRightToLeft(d,null); - } catch(Exception e) { - System.out.println("SKIPED:"+d); + } catch (RuntimeException e) { + TextToolsPlugin.getDefault().getLog().error("Failed to apply diff while saving edit", e); } }