let output_format = options.output_format;
let externs = options.externs.clone();
let scrape_examples_options = options.scrape_examples_options.clone();
let output_format = options.output_format;
let externs = options.externs.clone();
let scrape_examples_options = options.scrape_examples_options.clone();