GNOME Bugzilla – Bug 737876
gnome-user-docs does not always use <gui> for buttons adding/removing entries.
Last modified: 2014-10-04 22:49:28 UTC
In several pages the + and - buttons are referred to as <key>+</key> and <key>-</key> when they are not really keys on the keyboard but GUI elements and therefore ought to be referred to by <gui>+</gui> and <gui>-</gui>.
Created attachment 287705 [details] [review] Proposed patch.
Thank you very much for the bug report and the patch. I've applied this patch, and the fixes are present in commit 1e54990e73034df3c811f209dfe5f5c27b601d47.