From 68fb3e605e11c77d9c048417efdba31c6387d45f Mon Sep 17 00:00:00 2001
From: Florent Pruvost <florent.pruvost@inria.fr>
Date: Mon, 2 Oct 2017 16:29:27 +0200
Subject: [PATCH] pushing branch with -f is dangerous

---
 CONTRIBUTING.org | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/CONTRIBUTING.org b/CONTRIBUTING.org
index 5736ded9b..18bab331a 100644
--- a/CONTRIBUTING.org
+++ b/CONTRIBUTING.org
@@ -35,10 +35,8 @@
    Apply your modifications in that "Feature" branch. Then, you need
    to push this branch on your online repository
    #+begin_src sh
-   git push -f origin your_branch_name
+   git push origin your_branch_name
    #+end_src
-   or without -f, if the branch already exists online, and you just
-   want to update it.
 
 ** Merge request
    Once your branch is online, on the gitlab interface, go to the
-- 
GitLab