| changeset 76101 | e59d7d6fe1bd |
| parent 73599 | 981df2e1f646 |
| child 79749 | a861b0df74b4 |
--- 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"