Add -doc-stats options to print document statistics.
authorKim Nguyễn <kn@lri.fr>
Fri, 4 May 2012 14:00:11 +0000 (16:00 +0200)
committerKim Nguyễn <kn@lri.fr>
Fri, 4 May 2012 14:00:11 +0000 (16:00 +0200)
commit0da8c3c7c76ab06d5ccfc6ae52488d7549735059
treec5d9121550ff35f6c6d9c9da073df836f9407f3e
parent50da4f8d437372ae53be11a68beb424b35b28966
Add -doc-stats options to print document statistics.
src/main.ml
src/options.ml
src/options.mli
src/tree.ml