ti-linux-xenomai-4.19.y doesn't build

[giuliomoro]

I get

  MODPOST vmlinux.o
/home/giulio/bela-image-builder-stretch/downloads/ti-linux-kernel-dev/dl/gcc-8.4.0-nolibc/arm-linux-gnueabi/bin/arm-linux-gnueabi-ld: arch/arm/xenomai/machine.o: in function `mach_arm_calibrate':
machine.c:(.text+0x44): undefined reference to `__ipipe_mach_get_tsc'
/home/giulio/bela-image-builder-stretch/downloads/ti-linux-kernel-dev/dl/gcc-8.4.0-nolibc/arm-linux-gnueabi/bin/arm-linux-gnueabi-ld: machine.c:(.text+0x4c): undefined reference to `__ipipe_mach_get_tsc'
/home/giulio/bela-image-builder-stretch/downloads/ti-linux-kernel-dev/dl/gcc-8.4.0-nolibc/arm-linux-gnueabi/bin/arm-linux-gnueabi-ld: machine.c:(.text+0x78): undefined reference to `__ipipe_mach_get_tsc'
/home/giulio/bela-image-builder-stretch/downloads/ti-linux-kernel-dev/dl/gcc-8.4.0-nolibc/arm-linux-gnueabi/bin/arm-linux-gnueabi-ld: machine.c:(.text+0x8c): undefined reference to `__ipipe_mach_get_tsc'
/home/giulio/bela-image-builder-stretch/downloads/ti-linux-kernel-dev/dl/gcc-8.4.0-nolibc/arm-linux-gnueabi/bin/arm-linux-gnueabi-ld: kernel/xenomai/clock.o: in function `xnclock_core_read_monotonic':
(.text+0x2dc): undefined reference to `__ipipe_mach_get_tsc'
/home/giulio/bela-image-builder-stretch/downloads/ti-linux-kernel-dev/dl/gcc-8.4.0-nolibc/arm-linux-gnueabi/bin/arm-linux-gnueabi-ld: kernel/xenomai/clock.o:clock.c:(.text+0x414): more undefined references to `__ipipe_mach_get_tsc' follow
Makefile:1033: recipe for target 'vmlinux' failed
make[3]: *** [vmlinux] Error 1
debian/rules:6: recipe for target 'build' failed
make[2]: *** [build] Error 2
dpkg-buildpackage: error: debian/rules build subprocess returned exit status 2
scripts/package/Makefile:79: recipe for target 'bindeb-pkg' failed
make[1]: *** [bindeb-pkg] Error 2
Makefile:1365: recipe for target 'bindeb-pkg' failed
make: *** [bindeb-pkg] Error 2

.config file attached defconfig.zip

[giuliomoro]

but it does build with the default config file ...