src/Tools/GraphBrowser/graphbrowser/ParseError.java
changeset 74015 12b1f4649ab1
parent 74011 1d366486a812
equal deleted inserted replaced
74014:3b8b1da2ff29 74015:12b1f4649ab1
       
     1 package isabelle.graphbrowser;
       
     2 
       
     3 class ParseError extends Exception {
       
     4 	public ParseError(String s) { super(s); }
       
     5 }