# HG changeset patch
# User blanchet
# Date 1326821136 -3600
# Node ID 1a0b8f529b96e92e3d9dde3d52c3e235da0eea0b
# Parent  933f35c4e1260b3f729003527082bf689a5b3add
allow use of proxy for remote SMT solver invocations, just like in the "remote_atp" script

diff -r 933f35c4e126 -r 1a0b8f529b96 src/HOL/Tools/ATP/scripts/remote_atp
--- a/src/HOL/Tools/ATP/scripts/remote_atp	Tue Jan 17 16:30:54 2012 +0100
+++ b/src/HOL/Tools/ATP/scripts/remote_atp	Tue Jan 17 18:25:36 2012 +0100
@@ -92,6 +92,7 @@
 # Query Server
 my $Agent = LWP::UserAgent->new;
 $Agent->env_proxy;
+$Agent->agent("Sledgehammer");
 if (exists($Options{'t'})) {
   # give server more time to respond
   $Agent->timeout($Options{'t'} + 15);
diff -r 933f35c4e126 -r 1a0b8f529b96 src/HOL/Tools/SMT/lib/scripts/remote_smt
--- a/src/HOL/Tools/SMT/lib/scripts/remote_smt	Tue Jan 17 16:30:54 2012 +0100
+++ b/src/HOL/Tools/SMT/lib/scripts/remote_smt	Tue Jan 17 18:25:36 2012 +0100
@@ -19,6 +19,7 @@
 # call solver
 
 my $agent = LWP::UserAgent->new;
+$agent->env_proxy;
 $agent->agent("SMT-Request");
 $agent->timeout(180);
 my $response = $agent->post($ENV{"ISABELLE_SMT_REMOTE_URL"}, [