Add ci/extract-configure-log.sh

diff --git a/ci/extract-configure-log.sh b/ci/extract-configure-log.sh
new file mode 100755 (executable)
index 0000000..f5ea2a8
--- /dev/null
+++ b/ci/extract-configure-log.sh
@@ -0,0 +1,13 @@
+#!/usr/bin/awk -f
+
+/will be compiled with the following:/,/^  criterion:     No/ {
+    enable = 1;
+}
+{
+    if (enable) {
+        print $0;
+    }
+}
+/^  criterion:     No/ {
+    enable = 0;
+}