<html><head><style type="text/css"><!-- DIV {margin:0px;} --></style></head><body><div style="font-family:times new roman, new york, times, serif;font-size:12pt">Hi, was there something wrong with this patch?<br>(rediffed now against current git)<br></div><br>
</body></html>