ryanyao/freeleaps-pub
1
0
Fork 0
forked from freeleaps/freeleaps-pub
Code Pull Requests Activity

Update for redis cleanup when deinit

Browse Source
This commit is contained in:
timqiu 2025-03-10 10:29:50 +08:00
parent 3d483a3b99
commit 86226130b6
1 changed files with 45 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

81
devbox/devbox.local/cli/devbox
View File

@ -853,46 +853,46 @@ devbox_init_command() {
popd > /dev/null
fi
else
if ! echo "$USE_CUSTOM_REPOSITORY" | grep -Eq '^(https:\/\/|git@|git:\/\/|file:\/\/\/)[^ ]+\.git$'; then
echo "ERROR: Invalid custom repository URL. Please provide a valid URL."
else
if ! echo "$USE_CUSTOM_REPOSITORY" | grep -Eq '^(https:\/\/|git@|git:\/\/|file:\/\/\/)[^ ]+\.git$'; then
echo "ERROR: Invalid custom repository URL. Please provide a valid URL."
exit 1
fi
# Check if the custom repository is a git repository
# Test if the user can access the custom repository
echo "==> Testing access to custom repository..."
if ! git ls-remote "$USE_CUSTOM_REPOSITORY" &>/dev/null; then
echo "ERROR: Failed to access custom repository. Please check the repository URL."
echo "==> [INIT] DevBox environment initialization completed successfully, but access to the custom repository failed."
exit 1
fi
fi
CUSTOM_FOLDER_NAME=$(basename "$USE_CUSTOM_REPOSITORY" .git)
CUSTOM_DIR="$WORKING_HOME/$CUSTOM_FOLDER_NAME"
if [ ! -d "$CUSTOM_DIR" ]; then
pushd "$WORKING_HOME" > /dev/null
echo "Git cloning custom repository: $USE_CUSTOM_REPOSITORY"
git clone --depth 5 "$USE_CUSTOM_REPOSITORY"
else
pushd "$CUSTOM_DIR" > /dev/null
# Check $WORKING_HOME/custom exists and it is a git repository, if not git clone it
if ! git rev-parse --is-inside-work-tree &>/dev/null; then
popd > /dev/null # Exit from $CUSTOM_DIR
rm -rf "$CUSTOM_DIR" # Remove $CUSTOM_DIR
rmdir "$CUSTOM_DIR" # Remove $CUSTOM_DIR
# Test if the user can access the custom repository
echo "==> Testing access to custom repository..."
if ! git ls-remote "$USE_CUSTOM_REPOSITORY" &>/dev/null; then
echo "ERROR: Failed to access custom repository. Please check the repository URL."
echo "==> [INIT] DevBox environment initialization completed successfully, but access to the custom repository failed."
exit 1
fi
# Git clone custom repository
echo "Cloning repository again: $USE_CUSTOM_REPOSITORY"
sudo chown -R "$OWNER_GROUP" "$WORKING_HOME"
git clone --depth 5 "$USE_CUSTOM_REPOSITORY"
else
echo "Git pulling custom repository"
git pull
fi
CUSTOM_FOLDER_NAME=$(basename "$USE_CUSTOM_REPOSITORY" .git)
CUSTOM_DIR="$WORKING_HOME/$CUSTOM_FOLDER_NAME"
if [ ! -d "$CUSTOM_DIR" ]; then
pushd "$WORKING_HOME" > /dev/null
echo "Git cloning custom repository: $USE_CUSTOM_REPOSITORY"
git clone --depth 5 "$USE_CUSTOM_REPOSITORY"
else
pushd "$CUSTOM_DIR" > /dev/null
# Check $WORKING_HOME/custom exists and it is a git repository, if not git clone it
if ! git rev-parse --is-inside-work-tree &>/dev/null; then
popd > /dev/null # Exit from $CUSTOM_DIR
rm -rf "$CUSTOM_DIR" # Remove $CUSTOM_DIR
rmdir "$CUSTOM_DIR" # Remove $CUSTOM_DIR
# Git clone custom repository
echo "Cloning repository again: $USE_CUSTOM_REPOSITORY"
sudo chown -R "$OWNER_GROUP" "$WORKING_HOME"
git clone --depth 5 "$USE_CUSTOM_REPOSITORY"
else
echo "Git pulling custom repository"
git pull
fi
popd > /dev/null
fi
popd > /dev/null
fi
fi
pushd $DOVBOX_CLI_DIR > /dev/null
@ -1410,6 +1410,15 @@ devbox_deinit_command() {
rm -f "$WORKING_HOME/.mongodb-instance"
fi
if [[ -f "$WORKING_HOME/.redis-instance" ]]; then
local redis_container_id
redis_container_id=$(cat "$WORKING_HOME/.redis-instance")
echo "==> Stopping and removing Redis container: $redis_container_id"
docker stop "$redis_container_id" &>/dev/null || true
docker rm "$redis_container_id" &>/dev/null || true
rm -f "$WORKING_HOME/.redis-instance"
fi
# Stop and remove RabbitMQ container
if [[ -f "$WORKING_HOME/.rabbitmq-instance" ]]; then
local rabbitmq_container_id