From 7f8e139413e1bca2d7fd26da6022b85d5b645c86 Mon Sep 17 00:00:00 2001
From: Lorenzo Manacorda <lorenzo@mailbox.org>
Date: Sat, 9 Feb 2019 17:06:51 +0100
Subject: [PATCH] doc: remove extraneous contrib element

`contrib` is "A summary of the contributions made to a document by a
credited source", which we don't need in this case.
---
 doc/man-pages.xml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/doc/man-pages.xml b/doc/man-pages.xml
index d9bb7df28..616c2ef29 100644
--- a/doc/man-pages.xml
+++ b/doc/man-pages.xml
@@ -3,9 +3,7 @@
            xmlns:xi="http://www.w3.org/2001/XInclude">
  <title>Home Manager Reference Pages</title>
  <info>
-  <author><personname>Home Manager contributors</personname>
-   <contrib>Author</contrib>
-  </author>
+  <author><personname>Home Manager contributors</personname></author>
   <copyright><year>2017–2019</year><holder>Home Manager contributors</holder>
   </copyright>
  </info>