drive remove_from_queue with DeadGMPids

...instead of LiveGMPids

The latter may be out of date s.t. it contains fewer pids than are
actually alive, due to new GMs having sprung into live recently. We'd
then, incorrectly, remove the corresponding entries from the queue's
mnesia record, causing havoc.

DeadGMPids can be out of date too; it may contain fewer pids than have
actually died, due to GMs having died more recently. That is harmless
though since it never leads us to remove an entry that we shouldn't,
and we will learn about any new deaths eventually.

0 files changed, 0 insertions, 0 deletions