Dear all,
we still have a few open pull requests. Almost all of them are now in
conflict with the master branch. What is the best practice in this case?
Merge them with master from time to time? Or wait until someone deals with
them?
I am asking because of #852 and #692. They involve a series of rather
important bugfixes, but could not be merged at the current point in time.
Best,
Johannes