Update auf 1.13.0

1 files changed, 7 insertions, 4 deletions

diff --git a/maintenance/fetchText.php b/maintenance/fetchText.php
index 3b745c0a..91b78be3 100644
--- a/maintenance/fetchText.php
+++ b/maintenance/fetchText.php
@@ -1,7 +1,9 @@
 <?php
-
 /**
  * Communications protocol...
+ *
+ * @file
+ * @ingroup Maintenance
  */
 
 require "commandLine.inc";
@@ -10,6 +12,10 @@ $db = wfGetDB( DB_SLAVE );
 $stdin = fopen( "php://stdin", "rt" );
 while( !feof( $stdin ) ) {
 	$line = fgets( $stdin );
+	if( $line === false ) {
+		// We appear to have lost contact...
+		break;
+	}
 	$textId = intval( $line );
 	$text = doGetText( $db, $textId );
 	echo strlen( $text ) . "\n";
@@ -31,6 +37,3 @@ function doGetText( $db, $id ) {
 	}
 	return $text;
 }
-
-
-?>
\ No newline at end of file