From a73c43028027f19b7e244d52b57265b0c0ecf249 Mon Sep 17 00:00:00 2001
From: Andrew McMillan <debian@mcmillan.net.nz>
Date: Mon, 20 Nov 2006 22:38:27 +1300
Subject: [PATCH] Use the right options when we are making a "HEAD" request. 
 Much faster.

---
 testing/dav_test | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/testing/dav_test b/testing/dav_test
index 13d8542e..ab92e6f6 100755
--- a/testing/dav_test
+++ b/testing/dav_test
@@ -12,6 +12,7 @@ my @arguments = ( "--basic", "--proxy", "", "--silent" );
 push @arguments, "--verbose" if ( defined($ARGV[2]) );
 
 my $url;
+my $is_head_request = 0;
 my @auth = ( "--user", "user1:user1" );
 
 my $datafile = "tests/$suite/$test.data";
@@ -41,7 +42,12 @@ while( <TEST> ) {
   };
 
   /^\s*TYPE\s*=\s*(\S.*)$/ && do {
-    push @arguments, "--request", $1;
+    if ( $1 eq "HEAD" ) {
+      $is_head_request = 1;
+    }
+    else {
+      push @arguments, "--request", $1;
+    }
   };
 
   /^\s*HEADER\s*=\s*(\S.*)$/ && do {
@@ -64,6 +70,8 @@ EOERROR
   exit (2);
 }
 
+push @arguments, "--head" if ( $is_head_request );
+
 push @arguments, @auth;
 
 if ( -f $datafile ) {
@@ -75,10 +83,10 @@ else {
 }
 
 
-# print @arguments;
-# print "\n";
 push @arguments, $url;
 
+print join " ", "curl", @arguments, "\n" if ( defined($ENV{'DEBUG'}) );
+
 open RESULTS, "-|", "curl", @arguments;
 while( <RESULTS> ) {
   print;