Now that I have read how ERRACTused to behave, I'm not so confident that I did the right thing by changing the behavior. Still, the documentation should match the current behavior. If I later revert the changes to the code, then I will also revert the changes to the manual.