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)