>> I would omit option 2 completely. It's too fragile IMHO; it might
>> easily happen that anchors get inadvertently omitted if sections
>> are moved around in a document.
>
> I can't see why this would be particularly the case. Also, this
> option could be implemented with a macro similar to the one used for
> option 3, except that the English text would end up expanded in
> @anchor{} instead of being ignored. To me, option 2 could be
> optional, but I think that we should still recommend it if the
> manual is the target of external cross-references from already
> translated manuals to give time to change the external manuals
> cross-references to the newly translated manual.
Using a macro this looks OK to me.
Werner