Follow-up Comment #2, sr #107880 (project administration): Yes, it is a bug. I have a dim recollection of asking Michael, or maybe it was Sylvain, for an option to disable that useless "Docs" menu item some time ago.
I trust Michael will get to it in due course.
_______________________________________________________
Reply to this item at:
<http://savannah.gnu.org/support/?107880>
_______________________________________________
Message sent via/by Savannah
http://savannah.gnu.org/
