[galaxy-dev] Renaming pages on the Galaxy wiki

Hi all, I just renamed a page on the wiki to fix a typo: https://wiki.galaxyproject.org/ToolsWitDependenciesInSameRepository now: https://wiki.galaxyproject.org/ToolsWithDependenciesInSameRepository I didn't see any option about setting up a redirection from the old URL (for pages linked to it, or external lines bookmarks etc). I've searched the wiki and fixed the only internal link to this page, but I can't see how to add a redirect. Is there an easy way to move a page & setup a redirection in one go? Peter