changeset 82142 | 508a673c87ac |
parent 80510 | bbeb2f2049aa |
--- a/src/Pure/Tools/server.scala Tue Feb 11 23:31:12 2025 +0100 +++ b/src/Pure/Tools/server.scala Wed Feb 12 00:40:57 2025 +0100 @@ -21,7 +21,7 @@ import java.io.{BufferedInputStream, BufferedOutputStream, InputStreamReader, OutputStreamWriter, IOException} -import java.net.{Socket, SocketException, SocketTimeoutException, ServerSocket, InetAddress} +import java.net.{Socket, ServerSocket, InetAddress} object Server {