fdprintf() Anyone?

Hi

I have been asked about support for some odd non-standard printf variants
which take an "int fd" instead of a "FILE *". These are the functions in
question.

int fdprintf (int fd, const char *format,...)
  Print formatted output to a file descriptor.

int fdiprintf (int fd, const char *format,...)
  Print formatted output to a file descriptor (integer-only, no float)

int vfdprintf (int fd, const char *format, va_list args)
  Print formatted output to a file descriptor using va_list.

int vfdiprintf (int fd, const char *format, va_list args)
  Print formatted output to a file descriptor using va_list (integer-only)

The documentation for NetBurner (
https://www.netburner.com/NBDocsTest/Developer/html/group__group_fdprintf.html)
has them prototyped in <fdprintf.h>. But the user is using a system where
they are in <fcntl.h>. Personally, I prefer the non-standard fdprintf.h. I
have qualms about considering them part of <stdio.h>

Does anyone have any experience with these functions? Happen to know where
an appropriately licensed implementation could be found.

Is there any interest in these eventually landing in newlib?

--joel sherrill
RTEMS