On 2/11/16 6:28 pm, Sebastian Huber wrote: > > should we do a > > git rm -r doc > > ? >
Yes, I will do this when we branch the docs repo. Chris _______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
