Use bash to call _within_dev.sh

diskuv · Nov 8, 2024 · caef94b · caef94b
1 parent 060cd8b
commit caef94b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/unix/_common_tool.sh b/unix/_common_tool.sh
@@ -135,7 +135,7 @@ exec_in_platform() {
     if [ -n "${PLATFORM_EXEC_PRE_DOUBLE:-}" ]; then
         ACTUAL_PRE_HOOK_DOUBLE="$PLATFORM_EXEC_PRE_DOUBLE"
     fi
-    printf "%s\n" "exec '$DKMLDIR'/vendor/drc/unix/_within_dev.sh -p '$_exec_dev_or_arch_helper_DKMLPLATFORM' -0 '${ACTUAL_PRE_HOOK_SINGLE:-}' -1 '${ACTUAL_PRE_HOOK_DOUBLE:-}' \\" > "$_exec_dev_or_arch_helper_CMDFILE"
+    printf "%s\n" "exec bash '$DKMLDIR'/vendor/drc/unix/_within_dev.sh -p '$_exec_dev_or_arch_helper_DKMLPLATFORM' -0 '${ACTUAL_PRE_HOOK_SINGLE:-}' -1 '${ACTUAL_PRE_HOOK_DOUBLE:-}' \\" > "$_exec_dev_or_arch_helper_CMDFILE"
 
     cat "$_exec_dev_or_arch_helper_CMDARGS" >> "$_exec_dev_or_arch_helper_CMDFILE"