simplified the origin book keeping

This commit is contained in:
hneemann 2017-07-21 16:31:44 +02:00
parent 12141c22b7
commit 1e64844442

View File

@ -62,9 +62,13 @@ public class ExceptionWithOrigin extends Exception {
* @return the origin of the error * @return the origin of the error
*/ */
public Set<File> getOrigin() { public Set<File> getOrigin() {
HashSet<File> s = new HashSet<>(); if (origin == null)
s.add(origin); return null;
return s; else {
HashSet<File> os = new HashSet<>();
os.add(origin);
return os;
}
} }
/** /**