# HG changeset patch
# User wenzelm
# Date 1649498636 -7200
# Node ID 7ae5df33ff230f007083e8e0b0cbdb01d2958e28
# Parent  b958e053d9939e3dfb50b34fbf4610e8e495126d
tuned --- avoid redundant patterns;

diff -r b958e053d993 -r 7ae5df33ff23 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Apr 09 12:02:38 2022 +0200
+++ b/src/Pure/Tools/server.scala	Sat Apr 09 12:03:56 2022 +0200
@@ -348,11 +348,7 @@
           }
         }
       }
-      catch {
-        case _: IOException => false
-        case _: SocketException => false
-        case _: SocketTimeoutException => false
-      }
+      catch { case _: IOException => false }
   }