From: Kim Nguyễn <kn@lri.fr>
Date: Sun, 21 Oct 2012 07:51:19 +0000 (+0200)
Subject: Merge branch 'master' into pretty-print
X-Git-Url: http://git.nguyen.vg/gitweb/?p=SXSI%2Fxpathcomp.git;a=commitdiff_plain;h=13a15353a161600575ff4b70eda2c7a0f024d969

Merge branch 'master' into pretty-print
---

13a15353a161600575ff4b70eda2c7a0f024d969
diff --cc src/options.ml
index 197982d,babad16..7307794
--- a/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