| author | wenzelm | 
| Sat, 10 Sep 2022 16:57:12 +0200 | |
| changeset 76108 | bdab17df07a9 | 
| 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: 
73599diff
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: 
73599diff
changeset | 4 | ISABELLE_BASH_PROCESS="$ISABELLE_BASH_PROCESS_HOME/platform_${ISABELLE_PLATFORM64}/bash_process"
 |