lib/browser/GraphBrowser/Console.java
changeset 18018 82206a6c75c0
parent 14981 e73f8140af78
child 33686 8e33ca8832b1
equal deleted inserted replaced
18017:f6abeac6dcb5 18018:82206a6c75c0
    11 
    11 
    12 package GraphBrowser;
    12 package GraphBrowser;
    13 
    13 
    14 import java.io.*;
    14 import java.io.*;
    15 import java.util.*;
    15 import java.util.*;
    16 import java.net.*;
       
    17 import awtUtilities.*;
       
    18 
    16 
    19 public class Console {
    17 public class Console {
    20 	Graph g;
    18 	Graph g;
    21 	String gfname;  
    19 	String gfname;  
    22 
    20