merged
authorwenzelm
Thu, 20 Oct 2016 23:42:41 +0200
changeset 64328 2284011c341a
parent 64323 20d15328b248 (current diff)
parent 64327 3e651d9ce601 (diff)
child 64329 8f9d27c89241
merged
--- a/etc/options	Thu Oct 20 19:39:27 2016 +0200
+++ b/etc/options	Thu Oct 20 23:42:41 2016 +0200
@@ -206,3 +206,6 @@
 
 option ssh_connect_timeout : real = 60
   -- "SSH connection timeout (seconds)"
+
+option ssh_alive_interval : real = 30
+  -- "time interval to keep SSH server connection alive (seconds)"
--- a/src/Pure/Admin/check_sources.scala	Thu Oct 20 19:39:27 2016 +0200
+++ b/src/Pure/Admin/check_sources.scala	Thu Oct 20 23:42:41 2016 +0200
@@ -15,6 +15,9 @@
     val file_pos = path.position
     def line_pos(i: Int) = Position.Line_File(i + 1, file_name)
 
+    if (space_explode('/', Word.lowercase(path.expand.split_ext._1.implode)).contains("aux"))
+      Output.warning("Illegal file-name on Windows" + Position.here(file_pos))
+
     val content = File.read(path)
 
     for { (line, i) <- split_lines(content).iterator.zipWithIndex }
--- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 20 19:39:27 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 20 23:42:41 2016 +0200
@@ -106,7 +106,8 @@
       Remote_Build("lxbroy10", options = "-m32 -M4 -N"),
       Remote_Build("macbroy2", options = "-m32 -M4"),
       Remote_Build("macbroy30", options = "-m32 -M2"),
-      Remote_Build("macbroy31", options = "-m32 -M2"))
+      Remote_Build("macbroy31", options = "-m32 -M2"),
+      Remote_Build("vmnipkow9", options = "-m32 -M1,2,4", shared_home = false))
 
   private def remote_build_history(rev: String, r: Remote_Build): Logger_Task =
   {
--- a/src/Pure/General/ssh.scala	Thu Oct 20 19:39:27 2016 +0200
+++ b/src/Pure/General/ssh.scala	Thu Oct 20 23:42:41 2016 +0200
@@ -41,6 +41,9 @@
   def connect_timeout(options: Options): Int =
     options.seconds("ssh_connect_timeout").ms.toInt
 
+  def alive_interval(options: Options): Int =
+    options.seconds("ssh_alive_interval").ms.toInt
+
 
   /* init context */
 
@@ -76,6 +79,7 @@
       val session = jsch.getSession(if (user == "") null else user, host, port)
 
       session.setUserInfo(No_User_Info)
+      session.setServerAliveInterval(alive_interval(options))
       session.setConfig("MaxAuthTries", "3")
 
       if (options.bool("ssh_compression")) {
@@ -172,7 +176,7 @@
         val line_buffer = new ByteArrayOutputStream(100)
         def line_flush()
         {
-          val line = line_buffer.toString(UTF8.charset_name)
+          val line = Library.trim_line(line_buffer.toString(UTF8.charset_name))
           progress(line)
           result += line
           line_buffer.reset