lib/browser/GraphBrowser/ParseError.java
author wenzelm
Sun, 08 Sep 2019 13:07:03 +0200
changeset 70674 29bb1ebb188f
parent 13973 9170772bf420
permissions -rw-r--r--
clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories);

package GraphBrowser;

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