From 096a6d203e43fa85fd8a5497efacbb4df710eaf0 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Thu, 9 Nov 2023 16:41:46 +0100
Subject: [PATCH] Remove unneeded SuppressWarnings
---
de.prob.core/src/de/prob/cli/CliStarter.java | 1 -
1 file changed, 1 deletion(-)
diff --git a/de.prob.core/src/de/prob/cli/CliStarter.java b/de.prob.core/src/de/prob/cli/CliStarter.java
index 67fc4206..1833f8be 100644
--- a/de.prob.core/src/de/prob/cli/CliStarter.java
+++ b/de.prob.core/src/de/prob/cli/CliStarter.java
@@ -186,7 +186,6 @@ public final class CliStarter {
}
}
- @SuppressWarnings("unchecked")
private void extractCliInformation(final BufferedReader input)
throws CliException {
final PortPattern portPattern = new PortPattern();
--
GitLab