src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java

 					text = String.valueOf(text3);
 				}
 							
 				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);
 		}
 	}

                               System.err.println("Unable to write file " + args[1]);
                             }
                         } 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]);
 		}
 	}