/* @@@ Really this should be out of line, but this also causes link
compatibility problems with the base ABI. This is slightly better
than duplicating code, however. */
/* @@@ Really this should be out of line, but this also causes link
compatibility problems with the base ABI. This is slightly better
than duplicating code, however. */