/* Moved into a separate source file -- can be eliminated later */ #include int *__get_errno_ptr(void) { return ___errno(); }