Done !
http://git.php.net/?p=web/doc-editor.git;a=commitdiff;h=e2714634978e725e17c69958de469756e6d4da7c
;)
Thanks, this little change will probably help some newcomers.
Oh yes, I missed that. Intuitively when looking for documentation I
would look for an item called "Help" because this is what it tends to
be called in desktop apps, so it may be worth renaming it to this, but
I suppose this is an issue that may warrant a little more
discussion/opinion from others.
Personally, I can fully agree with your opinion. Also, link "Documentation" in "Online Documentation Editor" might be confusing ;)
My $0.02