# HG changeset patch # User wenzelm # Date 1534077106 -7200 # Node ID 64fb127e33f785f201b9c6cc3c893eca539301c5 # Parent 91162dd89571fb9ddfa36844fdb1a16aea13adcf# Parent a6cc4302c380d16caf85b4cae46126cae7aed73a merged diff -r a6cc4302c380 -r 64fb127e33f7 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Sat Aug 11 17:33:00 2018 +0200 +++ b/src/Pure/Tools/dump.scala Sun Aug 12 14:31:46 2018 +0200 @@ -94,7 +94,7 @@ selection: Sessions.Selection = Sessions.Selection.empty): Process_Result = { if (Build.build_logic(options, logic, build_heap = true, progress = progress, - dirs = dirs, system_mode = system_mode) != 0) error(logic + " FAILED") + dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED") val dump_options = make_options(options, aspects) @@ -116,7 +116,7 @@ /* session */ val session = - Thy_Resources.start_session(dump_options, logic, session_dirs = dirs, + Thy_Resources.start_session(dump_options, logic, session_dirs = dirs ::: select_dirs, include_sessions = include_sessions, progress = progress, log = log) val theories_result = session.use_theories(use_theories, progress = progress)