src/Pure/System/session.scala
changeset 37132 10ef4da1c314
parent 37129 4c83696b340e
child 37689 628eabe2213a
     1.1 --- a/src/Pure/System/session.scala	Thu May 27 12:34:30 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Thu May 27 12:35:40 2010 +0200
     1.3 @@ -263,7 +263,7 @@
     1.4      {
     1.5        val now = currentTime
     1.6        flush_time match {
     1.7 -        case None => flush_time = Some(now + 100)
     1.8 +        case None => flush_time = Some(now + 100)   // FIXME output_delay property
     1.9          case Some(time) => if (now >= time) flush()
    1.10        }
    1.11      }