wrong doc message MediaWiki:Deletebatch-system-username

I don't think this is a mistake. The extension uses a special account name (i.e. a system user account) to run a script. The account's name is "Delete page script".

Jon Harald Søby (talk)23:44, 9 September 2018