minor documentation fix

6 jobs for docedit in 43 minutes and 41 seconds (queued for 3 seconds)