--- a/src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java Wed Nov 22 17:50:36 2023 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java Thu Nov 23 11:36:38 2023 +0100
@@ -45,7 +45,7 @@
String line, text = "";
try {
- rd = new BufferedReader(new InputStreamReader((new URL(fname)).openConnection().getInputStream()));
+ rd = new BufferedReader(new InputStreamReader((new URI(fname)).toURL().openConnection().getInputStream()));
} catch (Exception exn) {
rd = new FileReader(path + fname);
}