From b261554e8f372aa66a2827fd23cb31e92bf494a1 Mon Sep 17 00:00:00 2001 From: Andreas Suter Date: Fri, 31 Jan 2020 07:50:50 +0100 Subject: [PATCH] updated docu Conflicts: doc/html/searchindex.js