On 22/07/2017 06:30, Jiri Gaisler wrote:
> Can somebody review and merge this to rtems-tools.git?

Pushed. Thanks.

Chris
_______________________________________________
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Reply via email to