From 7c381f0483d497b27e23a307cf2015ba3b5dbe09 Mon Sep 17 00:00:00 2001
From: Robin De Schepper <robin.deschepper93@gmail.com>
Date: Tue, 16 Nov 2021 10:28:31 +0100
Subject: [PATCH] Fix type in contributing docs (#1762)

---
 doc/contrib/doc.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/contrib/doc.rst b/doc/contrib/doc.rst
index 237e9059..a567ba45 100644
--- a/doc/contrib/doc.rst
+++ b/doc/contrib/doc.rst
@@ -23,7 +23,7 @@ Update policy
 
 How to we decide if documentation is good? By observing how effective it is used
 in practice. If a question on Arbor (regardless of medium) is satisfactorily
-resolved (on both sides!) by with a pointer to the (relevant section in the) docs,
+resolved (on both sides!) with a pointer to the (relevant section in the) docs,
 the documentation was good. If, on the other hand, explanation was needed, the
 documentation was bad.
 
-- 
GitLab