On 07/13/2017 09:59 PM, Jan Kiszka wrote: > Hi Philippe, > > would it be possible to remove the generated docs from git? When doing > full-text searches, it's extremely unhandy to have them in history > (that's unfortunately too late now) and in the current repo (git grep). > Moreover, they add more and more bloat to the repo. > > I suppose you make use of them when generating release tarballs and for > pushing them to the webserver. But both could also be scripted, I'm sure. >
I agree, the need for such pre-built documentation in the tree disappeared when the same stuff could be found on the website. I'll drop this in 3.1. -- Philippe. _______________________________________________ Xenomai mailing list [email protected] https://xenomai.org/mailman/listinfo/xenomai
