Nicholas Joll Mon, 20 Jan 2020 10:18:29 -0800
I think think that, at most, the problem that I reported occurs only *occasionally*. So, my original bug report - which suggested a constant or at least frequent problem - was erroneous. Perhaps this bug report should be closed.
