<?php
-
/**
* Communications protocol...
+ *
+ * @file
+ * @ingroup Maintenance
*/
require "commandLine.inc";
$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";
}
return $text;
}
-
-
-?>
\ No newline at end of file