From b97603890d13f981817f63ad9f1181555eb26aa0 Mon Sep 17 00:00:00 2001
From: Olivier Sauter <Olivier.Sauter@epfl.ch>
Date: Tue, 13 Aug 2019 11:34:01 +0200
Subject: [PATCH] rename head README to README_developer

contains guidelines for git and contributors
---
 README => README_developer | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)
 rename README => README_developer (82%)

diff --git a/README b/README_developer
similarity index 82%
rename from README
rename to README_developer
index 7edeb69f..a29c4739 100644
--- a/README
+++ b/README_developer
@@ -9,9 +9,9 @@ git-hosted version currently under development for automated tests etc.
 * To propose changes:
  * Open an issue to discuss the matter (in gitlab project page -> issues)
  * Then open a branch to work on the issue. There are several ways to do this:
-  * Click on 'create branch' on the issue page on gitlab (then `git fetch` and `git checkout <branchname>`) 
+  * Click on 'create branch' on the issue page on gitlab (then `git fetch` and `git checkout <branchname>`)
   * In your local space, do `git checkout -b <branchname>` to create a new branch from your current `HEAD`.
- * When done, `git push` the branch and submit a merge request. 
+ * When done, `git push` the branch and submit a merge request.
   * The link to open the merge request is shown following the commit.
   * Assign someone (other than yourself) to review the merge request.
-  * Follow up on any questions/comments and optionally amend your branch (and re-push) to fix any new issues that arise.
\ No newline at end of file
+  * Follow up on any questions/comments and optionally amend your branch (and re-push) to fix any new issues that arise.
-- 
GitLab