tuned --- avoid redundant patterns;
authorwenzelm
Sat, 09 Apr 2022 12:03:56 +0200
changeset 75426 7ae5df33ff23
parent 75425 b958e053d993
child 75427 323481d143c6
tuned --- avoid redundant patterns;
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 }
   }