# HG changeset patch
# User wenzelm
# Date 1635621078 -7200
# Node ID 549019b4a808af1f8c4c36c3969c8f5255339e2c
# Parent  fde3a4a4f757322fe7ba8dde0b720fe8ad775c8e
more robust;

diff -r fde3a4a4f757 -r 549019b4a808 lib/Tools/getenv
--- 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