author | wenzelm |
Sat, 30 Oct 2021 21:11:18 +0200 | |
changeset 74644 | 549019b4a808 |
parent 74643 | fde3a4a4f757 |
child 74645 | 30eba7f9a8e9 |
lib/Tools/getenv | file | annotate | diff | comparison | revisions |
--- a/lib/Tools/getenv Sat Oct 30 21:07:20 2021 +0200 +++ b/lib/Tools/getenv Sat Oct 30 21:11:18 2021 +0200 @@ -77,5 +77,9 @@ if [ -n "$DUMP" ]; then export PATH_JVM="$(platform_path "$PATH")" - "$ISABELLE_PRINTENV" -0 > "$DUMP" + if [ -e "$ISABELLE_PRINTENV" ]; then + "$ISABELLE_PRINTENV" -0 > "$DUMP" + else + exit 2 + fi fi