Hi Steffen, > > It is a very good principle to put only real source files into a git > > repository, and no generated files. I will continue so. My > > successor might make a different decision, though. > > Sure, that is your decision.
It's also long-standing normal practice. It's a real pain to look at the differences between versions under *source* control and have them cluttered with noisy differences between built outputs. Cheers, Ralph.
