From 4774dfef41abbd3ec884dd5cd6c3c022ea946d78 Mon Sep 17 00:00:00 2001 From: dgelessus <dgelessus@users.noreply.github.com> Date: Mon, 24 Oct 2022 18:38:34 +0200 Subject: [PATCH] Fix missed getOsInfo call --- de.prob.core/src/de/prob/cli/CliStarter.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/de.prob.core/src/de/prob/cli/CliStarter.java b/de.prob.core/src/de/prob/cli/CliStarter.java index 6515932d..c612de78 100644 --- a/de.prob.core/src/de/prob/cli/CliStarter.java +++ b/de.prob.core/src/de/prob/cli/CliStarter.java @@ -345,8 +345,7 @@ public final class CliStarter { public void sendUserInterruptReference() { if (userInterruptReference != null) { try { - final OsSpecificInfo osInfo = getOsInfo(Platform.getOS(), - Platform.getOSArch()); + final OsSpecificInfo osInfo = getOsInfo(Platform.getOS()); final String command = getCliPath() + File.separator + osInfo.subdir + File.separator + osInfo.userInterruptCmd; -- GitLab