After one last-minute change, only HACKING was updated and not
hacking.html.in, so this patch synchronizes that.