Hi Gilles,

I just tested your new build option. Maybe I'm using it the wrong way,
but I stumbled over two quirks:

 o "make install-nodev" fails as it tries to install the kernel without
   being root. Actually, I only wanted to install the user space part,
   how can I do this separately? Or is this rather a use-case for the
   standard build?

 o On every "make", the prepare-kernel script is executed -
   intentionally? Maybe it would be better to provide a dedicated make
   target to trigger the update.

Thanks,
Jan

Attachment: signature.asc
Description: OpenPGP digital signature

_______________________________________________
Xenomai-core mailing list
Xenomai-core@gna.org
https://mail.gna.org/listinfo/xenomai-core

Reply via email to