--- a/run/html_line_ending_linux.html	Sun Aug 19 19:11:54 2007 +0000
+++ b/run/html_line_ending_linux.html	Sun Aug 19 19:15:01 2007 +0000
@@ -21,17 +21,17 @@
  *	 "blah blah (linenumber) blah blah"
  */
 void checkLineNumber(Object o){
-	char[] string=o.toString();
+	string x=o.toString();
 
 	int start;
-	for(start=0; start<string.length; start++){if(string[start]=='('){break;}
+	for(start=0; start<x.length; start++){if(x[start]=='('){break;}
 	}
 
 	int end;
-	for(end=string.length-1; end>start; end--){if(string[end]==')'){break;}}
+	for(end=x.length-1; end>start; end--){if(x[end]==')'){break;}}
 
 	assert(end-start==2);
-	assert(string[start+1]=='8');
+	assert(x[start+1]=='8');
 }
 	</CODE></pre></body>
 </html>