| author | Fabian Huch <huch@in.tum.de> |
| Fri, 10 Nov 2023 14:42:07 +0100 | |
| changeset 78969 | 1b05c2b10c9f |
| 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"
|