--- a/src/Pure/Tools/server_commands.scala Fri Mar 16 15:22:08 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala Fri Mar 16 15:43:56 2018 +0100
@@ -105,7 +105,7 @@
yield Args(build = build, print_mode = print_mode)
def command(progress: Progress, args: Args, log: Logger = No_Logger)
- : (JSON.Object.T, (String, Session)) =
+ : (JSON.Object.T, (String, Thy_Resources.Session)) =
{
val base_info = Session_Build.command(progress, args.build)._3
@@ -131,7 +131,7 @@
def unapply(json: JSON.T): Option[String] =
JSON.string(json, "session_id")
- def command(session: Session): (JSON.Object.T, Process_Result) =
+ def command(session: Thy_Resources.Session): (JSON.Object.T, Process_Result) =
{
val result = session.stop()
val result_json = JSON.Object("return_code" -> result.rc)