# HG changeset patch
# User wenzelm
# Date 1626433150 -7200
# Node ID 027fb21bdd5d686092c41409a7cc5dfa6adc71fb
# Parent  12b1f4649ab1a92e20147c7b4e910a7a95112938
tuned --- fewer warnings;

diff -r 12b1f4649ab1 -r 027fb21bdd5d src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java
--- a/src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java	Fri Jul 16 12:55:02 2021 +0200
+++ b/src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java	Fri Jul 16 12:59:10 2021 +0200
@@ -109,7 +109,7 @@
 							
 				Frame f=new TextFrame(fname.substring(fname.lastIndexOf('/')+1),text);
 				f.setSize(500,600);
-				f.show();
+				f.setVisible(true);
 			}
 		} catch (Exception exn) {
 			System.err.println("Can't read file "+fname);
@@ -205,7 +205,7 @@
                         } else {
 			    f=new GraphBrowserFrame(gb);
 			    f.setSize(700,500);
-			    f.show();
+			    f.setVisible(true);
                         }
 		} catch (IOException exn) {
 			System.err.println("Can't open graph file "+args[0]);