# HG changeset patch
# User wenzelm
# Date 1476999761 -7200
# Node ID 2284011c341a959a6123756bfbfa185da220a1b7
# Parent  20d15328b248ef4c3157b02d8c38a9b08d2e4f0f# Parent  3e651d9ce601340eb7e933831bc21f546dc88351
merged

diff -r 20d15328b248 -r 2284011c341a etc/options
--- 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)"
diff -r 20d15328b248 -r 2284011c341a src/Pure/Admin/check_sources.scala
--- 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 }
diff -r 20d15328b248 -r 2284011c341a src/Pure/Admin/isabelle_cronjob.scala
--- 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 =
   {
diff -r 20d15328b248 -r 2284011c341a src/Pure/General/ssh.scala
--- 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