/* Not only is this the end of the options, but it's a
`quoted' region, which may have args that *look* like
options, so we definitely shouldn't try to use getopt past
/* Not only is this the end of the options, but it's a
`quoted' region, which may have args that *look* like
options, so we definitely shouldn't try to use getopt past