lib/browser/GraphBrowser/ParseError.java
author wenzelm
Wed, 08 Aug 2012 17:49:56 +0200
changeset 48738 f8c1a5b9488f
parent 13973 9170772bf420
permissions -rw-r--r--
simplified session specifications: names are taken verbatim and current directory is default;

package GraphBrowser;

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