From ec42b3eecd87b17170529253b37cd9e5c0a8ae01 Mon Sep 17 00:00:00 2001 From: Lukas Juhrich Date: Mon, 5 Dec 2022 21:01:04 +0100 Subject: [PATCH] [doc] fix headline --- doc/guides/setup.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/guides/setup.rst b/doc/guides/setup.rst index 3b341bdfc..83fdd20c9 100644 --- a/doc/guides/setup.rst +++ b/doc/guides/setup.rst @@ -2,7 +2,7 @@ Minimal setup ============= Using Docker ------- +------------ The full dev-setup requires docker. Follow the following guides: