Sebastian Kippe f05436e9b9
Fix mediawiki integration
Accidentally deleted a line in a recent PR, and it slipped through the
review.
2020-10-29 15:12:50 +01:00
..
2020-10-29 12:07:42 +01:00
2020-10-29 15:12:50 +01:00