# HG changeset patch # User wenzelm # Date 1342625248 -7200 # Node ID 62570361e608f197a2b95022959fc6d82b2bb209 # Parent 3592a2091c80d774532c80578a90abfd86fe2599 more errors; diff -r 3592a2091c80 -r 62570361e608 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Wed Jul 18 17:22:59 2012 +0200 +++ b/src/Pure/System/build.scala Wed Jul 18 17:27:28 2012 +0200 @@ -166,6 +166,11 @@ val full_name = if (entry.reset) entry.name else parent.name + "-" + entry.name + + if (entry.name == "") error("Bad session name") + if (infos.exists(_.name == full_name)) + error("Duplicate session name: " + quote(full_name)) + val path = entry.path match { case Some(p) => Path.explode(p) @@ -175,6 +180,7 @@ val info = Session_Info(dir + path, full_name, entry.parent, entry.description, entry.options, thys, entry.files) + infos += info } catch {