If nobody answers before Monday I'll look at Jenkins configs but I believe the corresponding make commands are explicitly called. I apologize but my phone is ringing... Regards Francis Dupont <fdupont at isc.org>