Oops, sorry, previous version of the patch has the Ubuntu GNU triplet in the table instead of the Debian one; amended.