>>>>> Jaromir Dolecek writes:

Jaromir> Urban Boquist wrote:
>>  Yes, but my problem, described in PR misc/8252, persists... :-(

Jaromir> Does the problem persist when you delete the Makefile you
Jaromir> mentioned in the PR ?

If I delete the Makefile then I lose my local modifications
(illustrated by the "echo apa" in the PR). So that wouldn't be a very
good idea.

The example in the PR, to revert to an older version of Makefile, was
simply to make the problem easily reproducible for others. The same
thing will happen if Makefile has been changed in the repository since
the last time I updated, and I try to get the latest version.

        -- Urban