Update auf 1.13.0

1 files changed, 7 insertions, 0 deletions

diff --git a/maintenance/counter.php b/maintenance/counter.php
index 67b9ce21..67575ec1 100644
--- a/maintenance/counter.php
+++ b/maintenance/counter.php
@@ -1,4 +1,11 @@
 <?php
+/**
+ * Helper file for update.php
+ *
+ * @file
+ * @ingroup Maintenance
+ */
+
 function print_c($last, $current) {
 	echo str_repeat( chr(8), strlen( $last ) ) . $current;
 }