allow use of proxy for remote SMT solver invocations, just like in the "remote_atp" script
authorblanchet
Tue, 17 Jan 2012 18:25:36 +0100
changeset 46241 1a0b8f529b96
parent 46240 933f35c4e126
child 46242 99a2a541c125
allow use of proxy for remote SMT solver invocations, just like in the "remote_atp" script
src/HOL/Tools/ATP/scripts/remote_atp
src/HOL/Tools/SMT/lib/scripts/remote_smt
--- 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);
--- 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"}, [