From bb367bc9e6407912f2255ded971151d275bf4ff2 Mon Sep 17 00:00:00 2001
From: "agentzh (Yichun Zhang)" <agentzh@gmail.com>
Date: Tue, 11 Jun 2013 16:51:26 -0700
Subject: [PATCH] util/dist-check: now we also check the --with-no-pool-patch
 option of the ./configure script.

---
 util/dist-check | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

diff --git a/util/dist-check b/util/dist-check
index 04301d9..8be584a 100755
--- a/util/dist-check
+++ b/util/dist-check
@@ -41,7 +41,23 @@ if ($opts{l}) {
 
 my $prefix;
 
-warn "=== Normal Build ===\n";
+warn "=== No Pool Build ===\n";
+$prefix = "/usr/local/openresty-nopool";
+unless ($opts{f}) {
+    sh "./configure --with-no-pool-patch $cfg_opts --prefix=$prefix -j$jobs > /dev/null";
+}
+sh "$make -j$jobs > /dev/null";
+sh "sudo $make install > /dev/null";
+sh "$prefix/nginx/sbin/nginx -V 2>&1 |grep $ver";
+#sh "$prefix/nginx/sbin/nginx -V 2>&1 |grep '\\--with-no-pool-patch'";
+system "sudo killall nginx > /dev/null 2>&1";
+sh "sudo $prefix/nginx/sbin/nginx";
+sh "curl -si localhost/lua|grep $lua";
+sh "curl -si localhost/lua|grep $ver";
+sh "curl -si localhost/lua|grep 'no pool'";
+sh "sudo $prefix/nginx/sbin/nginx -sstop";
+
+warn "\n=== Normal Build ===\n";
 $prefix = "/usr/local/openresty";
 unless ($opts{f}) {
     sh "./configure $cfg_opts -j$jobs > /dev/null";