edit timestamp

When using “edit timestamp” only the local timestamp is adjusted, the GMT one is not.
to fix, in post.php:
$datemodif_gmt = ", post_date = '".get_gmt_from_date("$aa-$mm-$jj $hh:$mn:$ss")."'";
should read
$datemodif_gmt = ", post_date_gmt = '".get_gmt_from_date("$aa-$mm-$jj $hh:$mn:$ss")."'";
(line 318 in current delta)
and
post_title = '$post_title'"
.$datemodif.","
Should be
post_title = '$post_title'"
.$datemodif_gmt
.$datemodif.","
(lines 342,343)
Someone in #wordpress helped me throught this yesterday, but I don’t remember who now.