--- 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