On 11/02/2015 10:36 AM, Pedro Alves wrote:
> $ grep -rn gl_cv_header_working_stdint_h
> config.cache:628:gl_cv_header_working_stdint_h=${gl_cv_header_working_stdint_h=no}
> config.log:39493:gl_cv_header_working_stdint_h=no
>
> But, I don't get a replacement:
>
> $ find . -name stdint.h
> $
>
> Any hints on where I should be looking next?
Hmm, I looked for how headers end up or not generated, and found out how that
makes it to the Makefile, and noticed that the stdint.h generation in my
Makefile
was commented out. Turns out my Makefile was stale, even after having done (I
believe) several config.status --recheck last night. Today I
re-ran "config.status", and lo, I get a replacement stdint.h.
Sorry for the false alarm.
Thanks,
Pedro Alves
