1.1 --- a/src/HOL/Tools/ATP/scripts/remote_atp	Tue May 24 10:03:15 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/scripts/remote_atp	Tue May 24 11:55:59 2011 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  
     1.5  #----Get format and transform options if specified
     1.6  my %Options;
     1.7 -getopts("hws:t:c:",\%Options);
     1.8 +getopts("hws:t:c:q:",\%Options);
     1.9  
    1.10  #----Usage
    1.11  sub usage() {
    1.12 @@ -36,6 +36,7 @@
    1.13    print("    -s<system>      ATP to use\n");
    1.14    print("    -t<time_limit>  CPU time limit for ATP\n");
    1.15    print("    -c<command>     custom ATP invocation command\n");
    1.16 +  print("    -q<num>         quietness level (0 = most verbose, 3 = least verbose)\n");
    1.17    print("    <file_name>     TPTP problem file\n");
    1.18    exit(0);
    1.19  }
    1.20 @@ -72,6 +73,10 @@
    1.21  if (exists($Options{'c'})) {
    1.22      $URLParameters{"Command___$System"} = $Options{'c'};
    1.23  }
    1.24 +#----Quietness
    1.25 +if (exists($Options{'q'})) {
    1.26 +    $URLParameters{"QuietFlag"} = "-q" . $Options{'q'};
    1.27 +}
    1.28  
    1.29  #----Get single file name
    1.30  if (exists($URLParameters{"ProblemSource"})) {