diff options
author | Benjamin Jones <bjones@galois.com> | 2013-02-12 15:46:34 -0800 |
---|---|---|
committer | Benjamin Jones <bjones@galois.com> | 2013-02-12 15:46:34 -0800 |
commit | f7a628b81b78d6973dd84ccb17c0ca08ad747401 (patch) | |
tree | 8b765dcf6543d1cb6ecc8b47ea282b5c7d8913e0 /headless | |
parent | ec8430327c7c5e85cbe229267f6ddb8a551e972f (diff) |
minor, System.exit upon run description parse errors
Diffstat (limited to 'headless')
-rw-r--r-- | headless/src/main/java/com/galois/fiveui/BasicCrawlerController.java | 1 | ||||
-rw-r--r-- | headless/src/main/java/com/galois/fiveui/HeadlessRunDescription.java | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/headless/src/main/java/com/galois/fiveui/BasicCrawlerController.java b/headless/src/main/java/com/galois/fiveui/BasicCrawlerController.java index b396776..79338ec 100644 --- a/headless/src/main/java/com/galois/fiveui/BasicCrawlerController.java +++ b/headless/src/main/java/com/galois/fiveui/BasicCrawlerController.java @@ -120,6 +120,7 @@ public class BasicCrawlerController { */ PageFetcher pageFetcher = new PageFetcher(config); RobotstxtConfig robotstxtConfig = new RobotstxtConfig(); + //robotstxtConfig.setEnabled(false); // uncomment if you want to ignore robots.txt RobotstxtServer robotstxtServer = new RobotstxtServer(robotstxtConfig, pageFetcher); CrawlController controller = new CrawlController(config, pageFetcher, robotstxtServer); diff --git a/headless/src/main/java/com/galois/fiveui/HeadlessRunDescription.java b/headless/src/main/java/com/galois/fiveui/HeadlessRunDescription.java index dd22343..92f2ef1 100644 --- a/headless/src/main/java/com/galois/fiveui/HeadlessRunDescription.java +++ b/headless/src/main/java/com/galois/fiveui/HeadlessRunDescription.java @@ -128,6 +128,7 @@ public class HeadlessRunDescription { atoms.add(HeadlessAtom.fromJsonObject(obj, ruleSetDir)); } catch (IOException e) { logger.error("HeadlessAtom.parse: error parsing ruleSet file: " + e.getMessage()); + System.exit(1); } catch (IllegalStateException e) { reportError(jsonElement); } |