tuned whitespace;
authorwenzelm
Thu, 06 Jun 2024 22:03:20 +0200
changeset 80271 198fc882ec0f
parent 80270 1d4300506338
child 80272 9f89b3c41460
tuned whitespace;
src/Pure/Build/build_manager.scala
src/Pure/System/bash.scala
--- a/src/Pure/Build/build_manager.scala	Thu Jun 06 21:48:36 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Thu Jun 06 22:03:20 2024 +0200
@@ -1153,7 +1153,7 @@
       List(pending, running, finished).foreach(dir =>
         sync_permissions(Isabelle_System.make_directory(dir)))
 
-    val ssh_group: String= options.string("build_manager_ssh_group")
+    val ssh_group: String = options.string("build_manager_ssh_group")
 
     def open_ssh(): SSH.Session =
       SSH.open_session(options,
--- a/src/Pure/System/bash.scala	Thu Jun 06 21:48:36 2024 +0200
+++ b/src/Pure/System/bash.scala	Thu Jun 06 22:03:20 2024 +0200
@@ -378,7 +378,7 @@
                 Isabelle_System.settings(
                   XML.Decode.list(XML.Decode.pair(XML.Decode.string, XML.Decode.string))(
                     YXML.parse_body(putenv))),
-              redirect= redirect)
+              redirect = redirect)
           }
           match {
             case Exn.Exn(exn) => reply_failure(exn)