It tok > > Pull :-) It should be fixed by commit > > 35c53bbcc8f0a7b8627a8d5a2e167d76dc52d1c4 . > > I pulled :-) and am building now. I will report the result (which will take a lot > of hours on this machine). It took some ours of hard work (for the machine) and it finished the build successfully :-) Thanks again! Winfried