author | wenzelm |
Wed, 26 Oct 2016 16:05:41 +0200 | |
changeset 64409 | 70c87ca55f2c |
parent 64408 | 50bcf976f276 |
child 64410 | 89da169f66fa |
--- a/src/Pure/Admin/isabelle_cronjob.scala Wed Oct 26 16:04:05 2016 +0200 +++ b/src/Pure/Admin/isabelle_cronjob.scala Wed Oct 26 16:05:41 2016 +0200 @@ -86,7 +86,7 @@ /* remote build_history */ - private sealed case class Remote_Build( + sealed case class Remote_Build( host: String, user: String = "", port: Int = SSH.default_port,