Fix for #399309

Just after I reported [#399309](https://bugs.eclipse.org/bugs/show_bug.cgi?id=399309), I noticed that everybody could contribute to the documentation...

Well, you can find a bugfix for that very bug in this request.