6237bb2f2f
These are cosmetic improvements spotted while working on the issue. 1. Do not waste time if there are no changes to notify about. 2. Fix the legacy plugin manager's get_plugins() call.