diff options
Diffstat (limited to 'recipes/jamvm/files/java')
| -rw-r--r-- | recipes/jamvm/files/java | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/recipes/jamvm/files/java b/recipes/jamvm/files/java deleted file mode 100644 index 0cc72cbed8..0000000000 --- a/recipes/jamvm/files/java +++ /dev/null @@ -1,15 +0,0 @@ -#!/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 - |