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

[Peter Wang]

On Sat, 19 Sep 2020 07:15:52 +1000 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> 
> 2020-09-18 13:03 GMT+10:00 "Peter Wang" <novalazy at gmail.com>:
> >> In that case, if there is an error, should the new predicates return 
> >> the option table as well, as it was just before the error?
> > 
> > Yes, I could see a use for that.
> 
> The attached diff does that. The log message also documents
> the diff creating the template, which I accidentally committed
> along with the changes to compiler/notes, since I don't fancy
> trying to do surgery on already-public git repositories.

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.

Use git push --force-with-lease to make sure someone else hasn't updated
the branch since you last fetched it.

Peter