Convert wikidot format to mediawiki using bash/sed. This is a cut down version of the script that was used to convert fancyclopedia.wikidot.com to fancyclopedia.org in mediawiki format, without lots of site specific detail. Its designed to show the kind of things that need to be done, its not a robust solution.