lib/browser/GraphBrowser/ParseError.java
author wenzelm
Thu, 25 Oct 2018 22:42:17 +0200
changeset 69188 2fd73a1a0937
parent 13973 9170772bf420
permissions -rw-r--r--
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv; proper update of jEdit environment -- avoid warnings in Java 11; activate jdk-11+28;

package GraphBrowser;

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