[patch] @ruser instead of @usermanref

[Graham Percival]

Could somebody apply git patch
bfc80559df5d5ad909e5b09615a607b3583f8687
to master? We now user @ruser to link to the user manual, instead of 
@usermanref.

(most GDP stuff won't be merged with master for a long time, but since 
these are distributed with the binary, it'll be a lot easier for us if 
the binary is updated with these)

Cheers,
- Graham