lib/browser/GraphBrowser/ParseError.java
author bulwahn
Tue, 14 Jun 2011 08:30:19 +0200
changeset 43379 8c4b383e5143
parent 13973 9170772bf420
permissions -rw-r--r--
quickcheck_narrowing returns some timing information

package GraphBrowser;

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