X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=options.mli;fp=options.mli;h=0000000000000000000000000000000000000000;hb=4b52da1a20a4fe031930bb96d2ca46bec06dc529;hp=3d9eda23917c2fe0ddcb195f5fe9d53255f48b85;hpb=a223af3254fb51c279cfbccdc18c59484fdca74e;p=SXSI%2Fxpathcomp.git

diff --git a/options.mli b/options.mli
deleted file mode 100644
index 3d9eda2..0000000
--- a/options.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-val parse_cmdline : unit -> unit 
-val index_empty_texts : bool ref
-val sample_factor : int ref
-val disable_text_collection : bool ref
-val count_only : bool ref
-val query : string ref
-val input_file : string ref
-val output_file : string option ref
-val save_file : string ref
-val time : bool ref
-val tc_threshold : int ref
-val backward : bool ref