avoid deprecated Scala;
authorwenzelm
Sat Oct 22 12:34:17 2016 +0200 (2016-10-22)
changeset 6434145b6faeee56d
parent 64340 7f42e66c0d3d
child 64342 53fb4a19fb98
avoid deprecated Scala;
src/Pure/Admin/build_log.scala
     1.1 --- a/src/Pure/Admin/build_log.scala	Fri Oct 21 21:03:17 2016 +0200
     1.2 +++ b/src/Pure/Admin/build_log.scala	Sat Oct 22 12:34:17 2016 +0200
     1.3 @@ -368,7 +368,7 @@
     1.4            case _ => Meta_Info.empty
     1.5          }
     1.6  
     1.7 -      case line :: _ if line.startsWith("\0") => Meta_Info.empty
     1.8 +      case line :: _ if line.startsWith("\u0000") => Meta_Info.empty
     1.9        case List(Isatest.End(_)) => Meta_Info.empty
    1.10        case _ :: AFP_Test.Bad_Init() :: _ => Meta_Info.empty
    1.11        case Nil => Meta_Info.empty