diff options
Diffstat (limited to 'recipes/jamvm/files')
| -rw-r--r-- | recipes/jamvm/files/java | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/recipes/jamvm/files/java b/recipes/jamvm/files/java new file mode 100644 index 0000000000..0cc72cbed8 --- /dev/null +++ b/recipes/jamvm/files/java @@ -0,0 +1,15 @@ +#!/bin/sh +# +# Wrapper which (almost) silently restarts the VM in case of segfaults. + +redo_from_start=1; +while [ $redo_from_start -eq 1 ]; do + echo "Running JamVM-native: ${@}" + redo_from_start=0; + jamvm ${1+"$@"} + if [ $? -eq 139 ]; then + echo "JamVM-native crashed - silently trying again" + redo_from_start=1; + fi +done + |