The addition of stdckdint.h to CREATED_HEADERS in Makefile.in leads to an error when installing loadable builtins on platforms that provide the header:
install: cannot stat '/tmp/bash/stdckdint.h': No such file or directory make[2]: *** [Makefile:903: install-headers] Error 1 make[2]: Leaving directory '/tmp/bash' make[1]: *** [Makefile:291: install-dev] Error 2 On platforms where the generated header is used, there is no error when installing, but the installed generated header is not usable since it #include's intprops-internal.h, which does not get installed. Paul's patch[1] used CREATED_CONFIGURE instead, which seems appropriate for avoiding these problems. [1]: https://lists.gnu.org/archive/html/bug-bash/2024-03/msg00085.html
