From c87f730fe4bc40f72ed5fa52fe032a7bdf2d549c Mon Sep 17 00:00:00 2001
From: msc- <github@callow.im>
Date: Fri, 13 Oct 2017 17:36:47 +0900
Subject: 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.
---
 src/pagedef.cpp | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/pagedef.cpp b/src/pagedef.cpp
index e797b050..2517942 100644
--- 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.}
-- 
cgit v0.12