lib/browser/GraphBrowser/ParseError.java
author wenzelm
Wed, 25 Jul 2012 12:38:54 +0200
changeset 48497 ba61aceaa18a
parent 13973 9170772bf420
permissions -rw-r--r--
some updates on "Building a repository version of Isabelle";

package GraphBrowser;

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