# HG changeset patch # User wenzelm # Date 1585307726 -3600 # Node ID 817e26a031987dac6108ac31eda32d098ac8457c # Parent 01d92325ddab512a4fddbcd3d9e70077741ebb0b tuned; diff -r 01d92325ddab -r 817e26a03198 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Fri Mar 27 12:13:39 2020 +0100 +++ b/src/Pure/Tools/build.scala Fri Mar 27 12:15:26 2020 +0100 @@ -281,14 +281,14 @@ val process = if (Sessions.is_pure(name)) { ML_Process(options, deps.sessions_structure, raw_ml_system = true, - cwd = info.dir.file, env = env, store = Some(store), args = (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten ::: - List("--eval", eval), + List("--eval", eval), + cwd = info.dir.file, env = env, store = Some(store), cleanup = () => args_file.delete) } else { - ML_Process(options, deps.sessions_structure, parent, List("--eval", eval), + ML_Process(options, deps.sessions_structure, logic = parent, args = List("--eval", eval), cwd = info.dir.file, env = env, store = Some(store), cleanup = () => args_file.delete) }