lib/browser/GraphBrowser/ParseError.java
author blanchet
Mon, 16 Mar 2015 23:00:38 +0100
changeset 59725 e5dc7e7744f0
parent 13973 9170772bf420
permissions -rw-r--r--
export more ML functions

package GraphBrowser;

class ParseError extends Exception {
	public ParseError(String s) { super(s); }
}