diff options
Diffstat (limited to 'src/JavaGUI2/de/uka')
| -rw-r--r-- | src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java index 9f6021535..988aee0a2 100644 --- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java @@ -113,7 +113,7 @@ class Printname { try { name = (String)this.paramNames.get(n); } catch (ArrayIndexOutOfBoundsException e) { - subcatLogger.warning(e.getLocalizedMessage()); + subcatLogger.fine(e.getLocalizedMessage()); } return name; } @@ -393,7 +393,7 @@ class Printname { + "<dd>" + this.paramTexts.get(which) + "</dd>"; return result; } catch (ArrayIndexOutOfBoundsException e) { - subcatLogger.warning(e.getLocalizedMessage()); + subcatLogger.fine(e.getLocalizedMessage()); return ""; } |