# HG changeset patch
# User wenzelm
# Date 1665829457 -7200
# Node ID fdf823f5b56f2625cd0fa91a9910de4a5237f051
# Parent  072e6c0a237358643f8fc9a7fbd83025868b02a5
tuned;

diff -r 072e6c0a2373 -r fdf823f5b56f src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Fri Oct 14 13:35:25 2022 +0200
+++ b/src/Pure/Tools/server_commands.scala	Sat Oct 15 12:24:17 2022 +0200
@@ -140,7 +140,7 @@
       val res =
         JSON.Object(
           "session_id" -> id.toString,
-          "tmp_dir" -> File.path(session.tmp_dir).implode)
+          "tmp_dir" -> session.tmp_dir_name)
 
       (res, id -> session)
     }