-# $Id: mk-1st.awk,v 1.107 2020/04/04 14:07:40 anonymous.maarten Exp $
+# $Id: mk-1st.awk,v 1.109 2020/08/31 23:49:24 tom Exp $
##############################################################################
# Copyright 2018,2020 Thomas E. Dickey #
# Copyright 1998-2016,2017 Free Software Foundation, Inc. #
}
printf "\t%s %s %s\n", program, src_name, dst_name
}
+function in_subset(value) {
+ value = " " value " ";
+ check = subset;
+ gsub("[+]", " ", check);
+ check = " " check " ";
+ return index(check,value);
+ }
BEGIN {
TOOL_PREFIX = "";
found = 0;
using = 0
if (subset == "none") {
using = 1
- } else if (index(subset,$2) > 0) {
+ } else if (in_subset($2) > 0) {
if (using == 0) {
if (found == 0) {
if ( name ~ /^.*\+\+.*/ ) {