changeset 27993 | 6dd90ef9f927 |
parent 27989 | a4fdc97cd2ff |
child 29140 | e7ac5bb20aed |
--- a/src/Pure/General/position.scala Mon Aug 25 16:52:11 2008 +0200 +++ b/src/Pure/General/position.scala Mon Aug 25 20:01:17 2008 +0200 @@ -22,7 +22,7 @@ case None => None case Some(value) => try { Some(Integer.parseInt(value)) } - catch { case e: NumberFormatException => None } + catch { case _: NumberFormatException => None } } }