| changeset 74644 | 549019b4a808 |
| parent 73581 | cd84e58aed26 |
| 74643:fde3a4a4f757 | 74644:549019b4a808 |
|---|---|
75 done |
75 done |
76 fi |
76 fi |
77 |
77 |
78 if [ -n "$DUMP" ]; then |
78 if [ -n "$DUMP" ]; then |
79 export PATH_JVM="$(platform_path "$PATH")" |
79 export PATH_JVM="$(platform_path "$PATH")" |
80 "$ISABELLE_PRINTENV" -0 > "$DUMP" |
80 if [ -e "$ISABELLE_PRINTENV" ]; then |
81 "$ISABELLE_PRINTENV" -0 > "$DUMP" |
|
82 else |
|
83 exit 2 |
|
84 fi |
|
81 fi |
85 fi |