[gnome-devel-docs/wip/swilmet/prog-guidelines] programming-guidelines: merging release commits

[Sébastien Wilmet <swilmet src gnome org>]

commit 05a349c1631daea721dfb0302a8df212f5a2310e
Author: Sébastien Wilmet <swilmet gnome org>
Date:   Sat Nov 7 14:34:10 2015 +0100

    programming-guidelines: merging release commits
    
    Absolutely requiring a linear Git history can be painful when doing
    releases. Re-running make distcheck is not the funniest thing to do and
    can take a long time (compiling the API documentation, running the
    tests, etc). So I think a small exception to the rule is acceptable.
    
    There was a discussion about that on the desktop-devel-list:
    https://mail.gnome.org/archives/desktop-devel-list/2014-July/msg00027.html
    the conclusion was that merging the release commit was the simplest
    solution.

 programming-guidelines/C/versioning.page |    6 +++++-
 1 files changed, 5 insertions(+), 1 deletions(-)
---
diff --git a/programming-guidelines/C/versioning.page b/programming-guidelines/C/versioning.page
index d9380a5..938d3bf 100644
--- a/programming-guidelines/C/versioning.page
+++ b/programming-guidelines/C/versioning.page
@@ -221,7 +221,11 @@ AC_SUBST([LT_VERSION],[0:0:0])</code>
         <list>
           <item><p>
             If that fails due to other commits having been pushed in the
-            meantime, restart at step 1
+            meantime, run <cmd>git pull</cmd> to merge your commit on the
+            branch followed by a second <cmd>git push</cmd>.  This is an
+            exception to the GNOME guideline to have a linear Git history
+            (<link xref="version-control#use-of-git"/>).  If you prefer to have
+            a linear history, you need to restart at step 1.
           </p></item>
         </list>
       </item>