Fix https://bugzilla.gnome.org/show_bug.cgi?id=782583.

Don't write both page name and title to NAME section of man page, if they are the same.
doxygen · Oct 13, 2017 · c87f730 · c87f730
1 parent bcf34f8
commit c87f730
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/src/pagedef.cpp b/src/pagedef.cpp
@@ -174,8 +174,11 @@ void PageDef::writeDocumentation(OutputList &ol)
     ol.writeString(" - ");
     ol.popGeneratorState();
 
-    ol.generateDoc(docFile(),docLine(),this,0,si->title,TRUE,FALSE,0,TRUE,FALSE);
-    ol.endSection(si->label,si->type);
+    if (si->title != manPageName)
+    {
+      ol.generateDoc(docFile(),docLine(),this,0,si->title,TRUE,FALSE,0,TRUE,FALSE);
+      ol.endSection(si->label,si->type);
+    }
   }
   ol.popGeneratorState();
   //2.}