# HG changeset patch
# User wenzelm
# Date 1663187052 -7200
# Node ID ff404465b20df6e63669b6778de95b045801822e
# Parent  e73025785dc7808c8f7b3b6a072a99383751ae79
unused;

diff -r e73025785dc7 -r ff404465b20d src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Wed Sep 14 22:24:06 2022 +0200
+++ b/src/Pure/General/ssh.scala	Wed Sep 14 22:24:12 2022 +0200
@@ -9,7 +9,6 @@
 
 
 import java.util.{Map => JMap}
-import java.net.ServerSocket
 
 
 object SSH {