changeset 71601 | 97ccf48c2f0c |
parent 71599 | 23d0a45a9283 |
child 71726 | a5fda30edae2 |
--- a/src/Pure/Tools/server_commands.scala Fri Mar 27 13:04:15 2020 +0100 +++ b/src/Pure/Tools/server_commands.scala Fri Mar 27 22:01:27 2020 +0100 @@ -49,7 +49,7 @@ : (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) = { val options = Options.init(prefs = args.preferences, opts = args.options) - val dirs = args.dirs.map(Path.explode(_)) + val dirs = args.dirs.map(Path.explode) val base_info = Sessions.base_info(options, args.session, progress = progress, dirs = dirs,