diff options
| author | hdaniels <unknown> | 2005-06-22 14:57:02 +0000 |
|---|---|---|
| committer | hdaniels <unknown> | 2005-06-22 14:57:02 +0000 |
| commit | 1f193ff830283f9630b216202bfb72acec9e7714 (patch) | |
| tree | a2ba44778b3b3066fafb04d28535a45712a99c9d /src/JavaGUI2 | |
| parent | 8d79dd035a58e4babfb5a1083a4cd276ea9dc4a9 (diff) | |
reduced log level if no param descriptions are present
Diffstat (limited to 'src/JavaGUI2')
| -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 ""; } |