BTW dev is also out of synch with master. All the PRs are getting
merged to master.

dev is no longer being used.  I would like to delete it.  But I want to make sure that no-one is use 'dev' before I do so.

Trying to maintain a dev branch in synchronization is nearly impossible.  It is better if all PRs come in on a new branch (like pr32).

I will delete the dev branch now.

Greg


Reply via email to