Closed rillig closed 2 years ago
@jeremiah Your comment seems to be off-topic for this commit. I just improved the command line, and the code already uses getopt, so I don't get your point.
getopt
The code I saw wasn't using getopt, but if this is off topic then feel free to ignore.
@dmgerman Are you interested in merging this pull request? Otherwise I'll delete it.
@jeremiah Your comment seems to be off-topic for this commit. I just improved the command line, and the code already uses
getopt
, so I don't get your point.