# HG changeset patch
# User blanchet
# Date 1387383991 -3600
# Node ID a77f18378b8fcf4b6285cb67ad6096fcf009b4f9
# Parent  41a109a00c532dc686bf7e84fe35ab9161fad217
changed pirate port

diff -r 41a109a00c53 -r a77f18378b8f src/HOL/Tools/ATP/scripts/remote_spass_pirate
--- a/src/HOL/Tools/ATP/scripts/remote_spass_pirate	Wed Dec 18 17:00:14 2013 +0100
+++ b/src/HOL/Tools/ATP/scripts/remote_spass_pirate	Wed Dec 18 17:26:31 2013 +0100
@@ -1,2 +1,2 @@
 #!/usr/bin/env bash
-curl -F file=@"$2" "http://91.228.53.68:8080/solve/pirate/"$1"s"
+curl -F file=@"$2" "http://91.228.53.68:51642/solve/pirate/"$1"s"