# HG changeset patch
# User blanchet
# Date 1298293184 -3600
# Node ID 98b3d5ce0935f528b5e65333b5293973489ed2e9
# Parent  0c6093d596d636d078810a2a0602a27bf4a57689
exit code 127 can mean many things -- not just (and probably not) Perl missing

diff -r 0c6093d596d6 -r 98b3d5ce0935 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Feb 21 11:50:38 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Feb 21 13:59:44 2011 +0100
@@ -478,8 +478,6 @@
 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
    these are sorted out properly in the SMT module, we have to interpret these
    ourselves. *)
-val perl_failures =
-  [(127, NoPerl)]
 val remote_smt_failures =
   [(22, CantConnect),
    (2, NoLibwwwPerl)]
@@ -495,8 +493,7 @@
 val unix_failures =
   [(139, Crashed)]
 val smt_failures =
-  perl_failures @ remote_smt_failures @ z3_wrapper_failures @ z3_failures @
-  unix_failures
+  remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures
 
 val internal_error_prefix = "Internal error: "