rename head README to README_developer

contains guidelines for git and contributors

README → 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.
+  * 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