Am Thu, 13 Jul 2017 21:59:06 +0200 schrieb "[ext] Jan Kiszka" <[email protected]>:
> 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 agree that it should not be in git. My solution is to remove them and i do not use git-grep anyways. For a working git-grep just do: "echo 'doc/**/*' >> .gitignore" Henning > 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 > _______________________________________________ Xenomai mailing list [email protected] https://xenomai.org/mailman/listinfo/xenomai
