Merge branch 'master' into pretty-print

diff --cc include/utils.ml
Simple merge

diff --cc src/options.ml
index 197982d,babad16..7307794
--- 1/src/options.ml
--- 2/src/options.ml
+++ b/src/options.ml
@@@ -1,26 -1,6 +1,5 @@@
 -open Utils
  open Format
- 
- let index_empty_texts = ref true
- let sample_factor = ref 64
- let disable_text_collection = ref false
- let tc_threshold = ref 60000
- 
- let query = ref ""
- let input_file = ref ""
- let output_file = ref None
- let save_file = ref ""
- let count_only = ref false
- let time = ref false
- let bottom_up = ref false
- let no_jump = ref false
- let no_cache = ref false
- let verbose = ref false
- let text_index_type = ref 0
- let do_perf = ref false
- let twopass = ref false
- let repeat = ref 1
- let docstats = ref false
- let no_wrap_results = ref false
+ open Config
  
  let set_index_type = function
    | "default" -> text_index_type := 0