From 0da9e7e72b0ce1866162f5b36075c601507139da Mon Sep 17 00:00:00 2001 From: welisheva22 Date: Fri, 24 May 2024 06:35:41 -0400 Subject: [PATCH] Update install-devtools.sh (#611) documentation fixed small typo Signed-off-by: welisheva22 --- hack/install-devtools.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hack/install-devtools.sh b/hack/install-devtools.sh index bb538c74..77edd623 100755 --- a/hack/install-devtools.sh +++ b/hack/install-devtools.sh @@ -3,7 +3,7 @@ set -e #-- docker/Python # Docker and python can be quite involved to get right (e.g., require sudo, -# setting up permissions, etc.), so we ask the user to install them manully. +# setting up permissions, etc.), so we ask the user to install them manually. # The devcontainer will install using apt-get, so that's probably ok for now. if [ -z "$(which docker)" ] || [ "$1" = "--force" ]; then echo "please install docker manually (https://docs.docker.com/engine/install/)"