On 2017-07-14 10:24, Henning Schild wrote: > 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"
This doesn't work, unfortunately. Jan _______________________________________________ Xenomai mailing list [email protected] https://xenomai.org/mailman/listinfo/xenomai
