1#!/usr/bin/awk -f
 2# extract linker version number from stdin and turn into single number
 3	{
 4	gsub(".*\\)", "");
 5	gsub(".*version ", "");
 6	gsub("-.*", "");
 7	split($1,a, ".");
 8	print a[1]*100000000 + a[2]*1000000 + a[3]*10000 + a[4]*100 + a[5];
 9	exit
10	}