This reverts commit 436a866f5d. This is not a good place for such auxiliary functionality; will be moved elsewhere.
436a866f5d