src/Pure/Tools/server_commands.scala
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,