# HG changeset patch
# User blanchet
# Date 1387286562 -3600
# Node ID cf38cffc3bd3cf16be2fcdcc06ef62bfc45181d5
# Parent  6ff7855a6cc20f69c9c0b291070d50b63e8717c2
removed workaround

diff -r 6ff7855a6cc2 -r cf38cffc3bd3 src/HOL/Tools/ATP/scripts/remote_spass_pirate
--- a/src/HOL/Tools/ATP/scripts/remote_spass_pirate	Tue Dec 17 14:15:23 2013 +0100
+++ b/src/HOL/Tools/ATP/scripts/remote_spass_pirate	Tue Dec 17 14:22:42 2013 +0100
@@ -1,3 +1,2 @@
 #!/usr/bin/env bash
-curl -F file=@"$2" "http://91.228.53.68:8080/solve/pirate/"$1"s" \
-  | sed "s/Invovled clauses/Involved clauses/"
+curl -F file=@"$2" "http://91.228.53.68:8080/solve/pirate/"$1"s"