diff -r 758fd2fbde1e -r e59d7d6fe1bd Admin/bash_process/etc/settings
--- a/Admin/bash_process/etc/settings	Fri Sep 09 20:48:18 2022 +0200
+++ b/Admin/bash_process/etc/settings	Fri Sep 09 21:15:11 2022 +0200
@@ -1,3 +1,4 @@
 # -*- shell-script -*- :mode=shellscript:
 
-ISABELLE_BASH_PROCESS="$COMPONENT/$ISABELLE_PLATFORM64/bash_process"
+ISABELLE_BASH_PROCESS_HOME="$COMPONENT"
+ISABELLE_BASH_PROCESS="$ISABELLE_BASH_PROCESS_HOME/platform_${ISABELLE_PLATFORM64}/bash_process"