Make "mini" the default alias for "thumb" in German
It's already "mini" in other languages.
The German Wikipedia community (which is obviously not the only German
one but the biggest) always complained a bit about the previously
used "miniatur". It's German, yes, but error-prone. The solution
was to add "mini". Which made most users happy as far as I can
tell after all these years.
My patch doesn't change anything except for one little detail:
The JavaScript call
mw.config.get( 'wgWikiEditorMagicWords' ).img_thumbnail
which is created in WikiEditorHooks::getMagicWords and used by
the WikiEditor extension will return "mini" instead of "miniatur".
Change-Id: I4e9ad3f2e56e08eaf3006a1af4b1c9746cd55715