X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Foptions.mli;h=57f142bacbbd694b531d26e4ff4e592a96a726a7;hb=a84e4fba7daf4f600958487d88f0b733fb19042e;hp=497f565cd39b33f67c6d7b9c24c16e593a24eed9;hpb=3627fb7a0e81c5104ab7d776ded6433349194990;p=SXSI%2Fxpathcomp.git diff --git a/src/options.mli b/src/options.mli index 497f565..57f142b 100644 --- a/src/options.mli +++ b/src/options.mli @@ -13,3 +13,4 @@ val bottom_up : bool ref val no_jump : bool ref val verbose : bool ref val text_index_type : int ref +val do_perf : bool ref