On 20 Feb 2013, Rupert Swarbrick wrote:
> [PS: I notice that Andreas Eder must have run into this problem in the
> past, given that he made a very similar change last January.
> Maybe we should have a hint in README.developers-howto ?]
Yes, unfortunately I cannot remember how the problem was fixed.
And lacking any working version of gcl I can no longer verify
things.
Sorry that I can't be of more help.
Andreas
--
ceterum censeo redmondinem esse delendam.