# HG changeset patch
# User wenzelm
# Date 1338306874 -7200
# Node ID 878de88db080473418ee922f19879bba079a0c2e
# Parent  63021e59cbf0dac3eeb81c682001cac8586214d2
tuned signature;

diff -r 63021e59cbf0 -r 878de88db080 src/Pure/General/properties.scala
--- a/src/Pure/General/properties.scala	Tue May 29 16:39:42 2012 +0200
+++ b/src/Pure/General/properties.scala	Tue May 29 17:54:34 2012 +0200
@@ -52,7 +52,7 @@
       props.find(_._1 == name).map(_._2)
   }
 
-  class Int(name: java.lang.String)
+  class Int(val name: java.lang.String)
   {
     def apply(value: scala.Int): T = List((name, Value.Int(value)))
     def unapply(props: T): Option[scala.Int] =
@@ -62,7 +62,7 @@
       }
   }
 
-  class Long(name: java.lang.String)
+  class Long(val name: java.lang.String)
   {
     def apply(value: scala.Long): T = List((name, Value.Long(value)))
     def unapply(props: T): Option[scala.Long] =
@@ -72,7 +72,7 @@
       }
   }
 
-  class Double(name: java.lang.String)
+  class Double(val name: java.lang.String)
   {
     def apply(value: scala.Double): T = List((name, Value.Double(value)))
     def unapply(props: T): Option[scala.Double] =