lib/browser/GraphBrowser/ParseError.java
author boehmes
Thu, 03 Sep 2009 22:47:31 +0200
changeset 32515 e7c0d3c0494a
parent 13973 9170772bf420
permissions -rw-r--r--
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform), removed PolyML.makestring (no strict dependency on PolyML anymore)

package GraphBrowser;

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