# HG changeset patch
# User wenzelm
# Date 1342723189 -7200
# Node ID aa1e730c3fdd50d839fa48d6bc5524bac4f2f34e
# Parent  bcce872202b3ec9acaeed94f67765739de61efd6
allow catalog entries to be commented-out;

diff -r bcce872202b3 -r aa1e730c3fdd src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Thu Jul 19 20:02:44 2012 +0200
+++ b/src/Pure/System/build.scala	Thu Jul 19 20:39:49 2012 +0200
@@ -193,7 +193,9 @@
 
   private def sessions_catalog(dir: Path, catalog: File, sessions: Session.Queue): Session.Queue =
   {
-    val dirs = split_lines(Standard_System.read_file(catalog)).filter(_ != "")
+    val dirs =
+      split_lines(Standard_System.read_file(catalog)).
+        filterNot(line => line == "" || line.startsWith("#"))
     (sessions /: dirs)((sessions1, dir1) =>
       try {
         val dir2 = dir + Path.explode(dir1)