diff --git a/compiler/core/src/zserio/tools/ExtensionManager.java b/compiler/core/src/zserio/tools/ExtensionManager.java index 20d550a68..d8a99f2f6 100644 --- a/compiler/core/src/zserio/tools/ExtensionManager.java +++ b/compiler/core/src/zserio/tools/ExtensionManager.java @@ -155,6 +155,11 @@ private File getWorkingDirectory() { decodedExecFile = new File(decodedExecUrlPath); } + if (decodedExecFile.getPath().startsWith("file:")) + { + decodedExecFile = new File(decodedExecFile.getPath().replaceFirst("^file:", "")); + } + System.out.println("decodedExecFile = " + decodedExecFile); System.out.println("decodedExecFile.getParentFile() = " + decodedExecFile.getParentFile()); System.out.println(