src/Pure/General/position.scala
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 }
     }
   }