/* moved into shared/htgif.c */