gif_deanimate(): Minor style fixes