# HG changeset patch
# User wenzelm
# Date 1477490741 -7200
# Node ID 70c87ca55f2c3d0f2a59c8ad1d6f8d8d1fae32ab
# Parent  50bcf976f276d6a7cc8a4ce731542b3908036c00
tuned signature -- more friendly for experimentation;

diff -r 50bcf976f276 -r 70c87ca55f2c src/Pure/Admin/isabelle_cronjob.scala
--- 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,