allow catalog entries to be commented-out;
authorwenzelm
Thu, 19 Jul 2012 20:39:49 +0200
changeset 49369aa1e730c3fdd
parent 49368 bcce872202b3
child 49370 6b36da29a0bf
allow catalog entries to be commented-out;
src/Pure/System/build.scala
     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)