# HG changeset patch
# User wenzelm
# Date 1587555902 -7200
# Node ID 21adf2ed442c6d302f6942c1bc5bc15bb9259b2a
# Parent  3875815f59677fc7a62589b1ae135b71f908fbc5
more informative error;

diff -r 3875815f5967 -r 21adf2ed442c 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)
   }