lib/browser/GraphBrowser/ParseError.java
author Lars Hupel <lars.hupel@mytum.de>
Sun, 17 Jul 2016 11:47:35 +0200
changeset 63519 78401d628718
parent 13973 9170772bf420
permissions -rw-r--r--
more precise error information for dynamic Scala tools

package GraphBrowser;

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