Index: parametric/so
===================================================================
--- parametric/so	(revision 21597)
+++ parametric/so	(revision 21598)
@@ -34,5 +34,7 @@
 
 #@@include common.awk
 
+#@@over@ignore:pin_*
+
 awk -f `dirname $0`/common.awk -f `dirname $0`/so.awk -v "args=$*" -v gen=`basename $0` -v "genfull=$0"