author | wenzelm |
Fri, 21 Jul 2023 10:56:11 +0200 | |
changeset 78421 | fd24f380b588 |
parent 76101 | e59d7d6fe1bd |
child 79749 | a861b0df74b4 |
permissions | -rw-r--r-- |
47799 | 1 |
# -*- shell-script -*- :mode=shellscript: |
2 |
||
76101
e59d7d6fe1bd
clarified directory names (e.g. for multi-platform remote execution): avoid being deleted via isabelle.Components.purge;
wenzelm
parents:
73599
diff
changeset
|
3 |
ISABELLE_BASH_PROCESS_HOME="$COMPONENT" |
e59d7d6fe1bd
clarified directory names (e.g. for multi-platform remote execution): avoid being deleted via isabelle.Components.purge;
wenzelm
parents:
73599
diff
changeset
|
4 |
ISABELLE_BASH_PROCESS="$ISABELLE_BASH_PROCESS_HOME/platform_${ISABELLE_PLATFORM64}/bash_process" |