On Tuesday, February 4, 2014 8:43:25 PM UTC+1, Bill Hart wrote: > > > > > On 4 February 2014 18:11, Jean-Pierre Flori <jpf...@gmail.com<javascript:> > > wrote: > >> >> >> On Tuesday, February 4, 2014 6:05:58 PM UTC+1, Jean-Pierre Flori wrote: >>> >>> >>> >>> On Tuesday, February 4, 2014 5:56:29 PM UTC+1, Bill Hart wrote: >>>> >>>> Hi all, >>>> >>>> from today until 28 Feb (incl.) I will be working exclusively on MPIR >>>> (with a couple of very small interruptions). >>>> >>>> Today I did the following: >>>> >>>> * cleaned up .gitignore to make git ignore all autogenerated files >>>> >>>> Great. I've been working on that lately. >>> There are some commits on my github branch. >>> I'll just rework on top of your updated branch. >>> >> > Sure. Let me know when you are ready and I'll merge them. > > >> >>> Note that from my point of view, nothing coming automatically produced >>> by autoreconf should be tracked in the git repo. >>> >> > Unfortunately I don't think we can do that. When we do make dist it > expects that there is a valid configure and Makefiles. Also, running > autoreconf throttles our hacked config.guess and config.sub. So it's not > quite trivial to regenerate everything. > > What if we store the config.* wrappers with different names (let's say configmpir.*), let autoreconf do its magic and update config.* and let the configure script move the autoreconfed config.* to configfsf.* and the configmpir.* to config.* first thing when executed?
It will be a little more painful when one wants to "make dist", but "autoreconf -fiv (--no-recursive); make dist" should then just work fine and we'll avoid all autoconf horrible commits. I'll give it a shot on my branches. -- You received this message because you are subscribed to the Google Groups "mpir-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to mpir-devel+unsubscr...@googlegroups.com. To post to this group, send email to mpir-devel@googlegroups.com. Visit this group at http://groups.google.com/group/mpir-devel. For more options, visit https://groups.google.com/groups/opt_out.
