diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Tools/server_commands.scala --- 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,