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. Jan -- Siemens AG, Corporate Technology, CT RDA ITP SES-DE Corporate Competence Center Embedded Linux _______________________________________________ Xenomai mailing list [email protected] https://xenomai.org/mailman/listinfo/xenomai
