diff -r 000000000000 -r 835178a32fc1 tools/extract-config.sh
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tools/extract-config.sh	Tue Jul 17 21:44:33 2007 +0000
@@ -0,0 +1,23 @@
+#!/bin/sh
+
+# This scripts extracts a crosstool-NG configuration from the log file
+# of a toolchain build with crosstool-NG.
+
+# Usage: cat <logfile> |$0
+
+awk '
+BEGIN {
+  dump = 0;
+}
+
+$0~/Dumping crosstool-NG configuration: done in.+s$/ {
+  dump = 0;
+}
+
+dump == 1 { $1 = "" }
+dump == 1
+
+$0~/Dumping crosstool-NG configuration$/ {
+  dump = 1;
+}
+' |cut -d ' ' -f 2-