# HG changeset patch
# User wenzelm
# Date 1700735798 -3600
# Node ID 22c41ee13939fd147708ba4c716687855831abfb
# Parent  7449ff77029eef83646f1fc527d43829a07fb769
avoid deprecated URL constructors;

diff -r 7449ff77029e -r 22c41ee13939 src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java
--- 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);
             }