ioeric added a comment. As per our offline discussion, `getchar()` does not work with options with more than 2 digits (e.g. index number > 9). I'll keep it as it is now until we come up with a better solution. http://reviews.llvm.org/D21019