void do_commandline(int argc, char *argv[]);


syntax highlighted by Code2HTML, v. 0.9.1