The current handling of cmdline arguments seem to simulate subcommands, which see a proper handling in cmdliner 1.1.0. (Incidentally, the current code triggers warnings if compiled with cmdliner 1.1.0 because it uses now-deprecated APIs)
Task: port the code to use the new APIs of cmdliner 1.1.0.
The current handling of cmdline arguments seem to simulate subcommands, which see a proper handling in cmdliner 1.1.0. (Incidentally, the current code triggers warnings if compiled with cmdliner 1.1.0 because it uses now-deprecated APIs)
Task: port the code to use the new APIs of cmdliner 1.1.0.