<?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";
if( $text === false ) {
return false;
}
- $stripped = str_replace( "\r", "", $text );
- $normalized = UtfNormal::cleanUp( $stripped );
- return $normalized;
+ return $text;
}
-
-
-?>
\ No newline at end of file