more informative error;
authorwenzelm
Wed, 22 Apr 2020 13:45:02 +0200
changeset 71780 21adf2ed442c
parent 71777 3875815f5967
child 71781 3fd54f7f52b0
more informative error;
src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Tue Apr 21 22:19:59 2020 +0200
+++ b/src/Pure/General/ssh.scala	Wed Apr 22 13:45:02 2020 +0200
@@ -13,7 +13,8 @@
 import scala.util.matching.Regex
 
 import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException,
-  OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS}
+  OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS,
+  JSchException}
 
 
 object SSH
@@ -78,8 +79,13 @@
 
     val identity_files =
       space_explode(':', options.string("ssh_identity_files")).map(Path.explode)
-    for (identity_file <- identity_files if identity_file.is_file)
-      jsch.addIdentity(File.platform_path(identity_file))
+    for (identity_file <- identity_files if identity_file.is_file) {
+      try { jsch.addIdentity(File.platform_path(identity_file)) }
+      catch {
+        case exn: JSchException =>
+          error("Error in ssh identity file " + identity_file + ": " + exn.getMessage)
+      }
+    }
 
     new Context(options, jsch)
   }