# HG changeset patch
# User wenzelm
# Date 1506853732 -7200
# Node ID 14889103646959cc83de6df01cbef2c0240d54b6
# Parent  5887ae5b95a805b2c9f23f9807f8f22a4b9ae517
more standard merge operation;

diff -r 5887ae5b95a8 -r 148891036469 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Sep 30 22:55:23 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Sun Oct 01 12:28:52 2017 +0200
@@ -373,14 +373,14 @@
     session_groups: List[String] = Nil,
     sessions: List[String] = Nil)
   {
-    def + (other: Selection): Selection =
+    def ++ (other: Selection): Selection =
       Selection(
         requirements = requirements || other.requirements,
         all_sessions = all_sessions || other.all_sessions,
-        exclude_session_groups = exclude_session_groups ::: other.exclude_session_groups,
-        exclude_sessions = exclude_sessions ::: other.exclude_sessions,
-        session_groups = session_groups ::: other.session_groups,
-        sessions = sessions ::: other.sessions)
+        exclude_session_groups = Library.merge(exclude_session_groups, other.exclude_session_groups),
+        exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions),
+        session_groups = Library.merge(session_groups, other.session_groups),
+        sessions = Library.merge(sessions, other.sessions))
 
     def apply(graph: Graph[String, Info]): (List[String], Graph[String, Info]) =
     {
diff -r 5887ae5b95a8 -r 148891036469 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Sep 30 22:55:23 2017 +0200
+++ b/src/Pure/Tools/build.scala	Sun Oct 01 12:28:52 2017 +0200
@@ -372,7 +372,7 @@
     val (selected, selected_sessions) =
       full_sessions.selection(
           Sessions.Selection(requirements, all_sessions, exclude_session_groups,
-            exclude_sessions, session_groups, sessions) + selection)
+            exclude_sessions, session_groups, sessions) ++ selection)
 
     val deps =
       Sessions.deps(selected_sessions, progress = progress, inlined_files = true,