From 0f31e622b22a601162032cda5c927f20cbce8070 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 24 Jan 2019 14:36:22 +0100
Subject: [PATCH] tweak docs some more

---
 CONTRIBUTING.md |  4 +++-
 README.md       | 23 +++++++++++------------
 2 files changed, 14 insertions(+), 13 deletions(-)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 00485b47d..fc450fc07 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -2,7 +2,9 @@
 
 ## How to submit a merge request
 
-To contribute code, please send your MPI-SWS GitLab username to
+To contribute code, you need an
+[MPI-SWS GitLab account](https://gitlab.mpi-sws.org/users/sign_in) (use the
+"Register" tab).  Please send your MPI-SWS GitLab username to
 [Ralf Jung](https://gitlab.mpi-sws.org/jung) to enable personal projects for
 your account.  Then you can fork the
 [Iris git repository](https://gitlab.mpi-sws.org/FP/iris-coq/), make your
diff --git a/README.md b/README.md
index dcd8aa088..e06d5ddd6 100644
--- a/README.md
+++ b/README.md
@@ -108,21 +108,20 @@ that should be compatible with this version:
 * [Iris Atomic](https://gitlab.mpi-sws.org/FP/iris-atomic/) is an experimental
   formalization of logically atomic triples in Iris.
 
-## Notes for Iris Developers
+## Further Resources
 
 * Information on how to set up your editor for unicode input and output is
   collected in [Editor.md](Editor.md).
 * The Iris Proof Mode (IPM) / MoSeL is documented at [ProofMode.md](ProofMode.md).
 * Naming conventions are documented at [Naming.md](Naming.md).
 * The generated coqdoc is [available online](https://plv.mpi-sws.org/coqdoc/iris/).
-
-Discussion about the Iris Coq development happens on the mailing list
-[iris-club@lists.mpi-sws.org](https://lists.mpi-sws.org/listinfo/iris-club) and
-in the [Iris Chat](https://mattermost.mpi-sws.org/iris).  This is also the right
-place to ask questions.  The chat requires an account at the
-[MPI-SWS GitLab](https://gitlab.mpi-sws.org/users/sign_in) (use the "Register"
-tab).  If you want to report a bug, please use the
-[issue tracker](https://gitlab.mpi-sws.org/FP/iris-coq/issues), which also
-requires an MPI-SWS GitLab account.
-
-To contribute to Iris itself, see the [contribution guide](CONTRIBUTING.md).
+* Discussion about the Iris Coq development happens on the mailing list
+  [iris-club@lists.mpi-sws.org](https://lists.mpi-sws.org/listinfo/iris-club)
+  and in the [Iris Chat](https://mattermost.mpi-sws.org/iris).  This is also the
+  right place to ask questions.  The chat requires an account at the
+  [MPI-SWS GitLab](https://gitlab.mpi-sws.org/users/sign_in) (use the "Register"
+  tab).
+* If you want to report a bug, please use the
+  [issue tracker](https://gitlab.mpi-sws.org/FP/iris-coq/issues), which also
+  requires an MPI-SWS GitLab account.
+* To contribute to Iris itself, see the [contribution guide](CONTRIBUTING.md).
-- 
GitLab