diff --git a/scripts/install_macos.sh b/scripts/install_macos.sh
index f45895008d4a0..eb3e0863ce886 100755
--- a/scripts/install_macos.sh
+++ b/scripts/install_macos.sh
@@ -14,17 +14,22 @@ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf
 elan toolchain install stable
 elan default stable
 
-# Install the universal darwin build of VS Code
-curl -L https://update.code.visualstudio.com/latest/darwin-universal/stable -o ~/Downloads/VSCode-darwin-universal.zip
+# Check if VS Code is available on the command line
+if ! command -v code &> /dev/null; then
+    # Install the universal darwin build of VS Code
+    curl -L https://update.code.visualstudio.com/latest/darwin-universal/stable -o ~/Downloads/VSCode-darwin-universal.zip
 
-# Unzip the downloaded file to the Applications folder
-unzip -o ~/Downloads/VSCode-darwin-universal.zip -d /Applications
+    # Unzip the downloaded file to the Applications folder
+    unzip -o ~/Downloads/VSCode-darwin-universal.zip -d /Applications
 
-# Add the VS Code binary to the PATH to enable launching from the terminal
-cat << EOF >> ~/.zprofile
+    # Add the VS Code binary to the PATH to enable launching from the terminal
+    cat >> ~/.zprofile << EOF
 # Add Visual Studio Code (code)
 export PATH="\$PATH:/Applications/Visual Studio Code.app/Contents/Resources/app/bin"
 EOF
+else
+    echo "VS Code is already installed."
+fi
 
 # Install the Lean4 VS Code extension
 code --install-extension leanprover.lean4