src/Pure/System/build.scala
changeset 48354 aa1e730c3fdd
parent 48352 7fbf98ee265f
child 48361 63bdba7c1366
     1.1 --- a/src/Pure/System/build.scala	Thu Jul 19 20:02:44 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Thu Jul 19 20:39:49 2012 +0200
     1.3 @@ -193,7 +193,9 @@
     1.4  
     1.5    private def sessions_catalog(dir: Path, catalog: File, sessions: Session.Queue): Session.Queue =
     1.6    {
     1.7 -    val dirs = split_lines(Standard_System.read_file(catalog)).filter(_ != "")
     1.8 +    val dirs =
     1.9 +      split_lines(Standard_System.read_file(catalog)).
    1.10 +        filterNot(line => line == "" || line.startsWith("#"))
    1.11      (sessions /: dirs)((sessions1, dir1) =>
    1.12        try {
    1.13          val dir2 = dir + Path.explode(dir1)