So while searching for how to rename a database in MySQL Workbench, I came across the duplicate-flagged "How do I rename a MySQL schema?", which has just one answer -- and that answer, as it happens, is the answer to my Workbench question.
It turns out the author of the answer misunderstood the OP, and what the OP was really asking was how to rename the database in MySQL -- a question which does, in fact, already have some answers.
Would it be appropriate to edit the question to match the (useful) answer, since otherwise the question will probably eventually be closed as a duplicate?