# HG changeset patch # User wenzelm # Date 1521927906 -3600 # Node ID 83902fff62439d01c1b6e2dd1ca8361872b19682 # Parent ad735a551a110115f079e3af9e27f4c3a764c61c clarified signature; diff -r ad735a551a11 -r 83902fff6243 src/Pure/Thy/thy_resources.scala --- a/src/Pure/Thy/thy_resources.scala Sat Mar 24 22:10:14 2018 +0100 +++ b/src/Pure/Thy/thy_resources.scala Sat Mar 24 22:45:06 2018 +0100 @@ -18,6 +18,7 @@ options: Options, session_name: String, session_dirs: List[Path] = Nil, + include_sessions: List[String] = Nil, session_base: Option[Sessions.Base] = None, print_mode: List[String] = Nil, progress: Progress = No_Progress, @@ -25,7 +26,8 @@ { val base = session_base getOrElse - Sessions.base_info(options, session_name, progress = progress, dirs = session_dirs).check_base + Sessions.base_info(options, session_name, include_sessions = include_sessions, + progress = progress, dirs = session_dirs).check_base val resources = new Thy_Resources(base, log = log) val session = new Session(session_name, options, resources)