Use Cmdliner for command-line parsing
Side-effects: - more uniform handling of --help and --version, automatic generation of Unix manpages - slight change in syntax (see demo.sh) - sub-commands of "election" (Tool_election) are now direct commands, "election" itself disappears - in Tool_election, concatenate with --dir option (if any) instead of calling chdir
src/tool/tool_common.ml
0 → 100644
src/tool/tool_common.mli
0 → 100644