From b0ddf4d704063b30772bd5a275f8411a15a09f84 Mon Sep 17 00:00:00 2001
From: Matthias Richter <matthias.ri97@gmail.com>
Date: Sat, 18 Nov 2023 04:26:19 +0100
Subject: [PATCH] fix(installation): avoid additional repository cloning in
 devcontainer setup

closes #1776
---
 .devcontainer/setup.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.devcontainer/setup.sh b/.devcontainer/setup.sh
index 0e090a86..c119ab81 100755
--- a/.devcontainer/setup.sh
+++ b/.devcontainer/setup.sh
@@ -4,4 +4,4 @@ curl https://sh.rustup.rs -sSf | sh -s -- -y
 # Update current shell environment variables after install to find rustup
 . "$HOME/.cargo/env"
 rustup install stable
-bash install.sh
+bash install.sh --no-clone