[m-rev.] for review: changes to option handling

[Zoltan Somogyi]

2020-09-19 10:36 GMT+10:00 "Peter Wang" <novalazy at gmail.com>:
> For next time, I think it's fine to force-push a fixed branch if you
> notice a mistake "soon" after you push a branch. Or force-push the
> previous latest commit, then take your time to fix it.

Thanks for that.

If the diff had been an ordinary diff that only changed files, I would have
tried to look for such a solution. Since it involved deleting and renaming
files, I did not have sufficient confidence in git's ability to handle that
without screwing up history to even try, because my experience is that
git is sometimes brilliant and sometimes extremely stupid. For example,
I am impressed that git recognized getopt_template as a modified version
of the old getopt_io.m, but I continue to be pissed off by git's inability,
or unwillingness, to stash changes after "git add -N".

Zoltan.