diff options
| -rw-r--r-- | dist/checkman.awk | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/dist/checkman.awk b/dist/checkman.awk index 4d682cab..a9c7436f 100644 --- a/dist/checkman.awk +++ b/dist/checkman.awk @@ -285,11 +285,15 @@ $1 != ".RE" { } sh == "SOURCE" && $1 ~ /^\// { - Sources[$1] = 1 + s = $1 + sub("\\\*9", ENVIRON["PLAN9"], s) + Sources[s] = 1 } sh == "SOURCE" && $2 ~ /^\// { - Sources[$2] = 1 + s = $2 + sub("\\\*9", ENVIRON["PLAN9"], s) + Sources[s] = 1 } $0 ~ /^\.[A-Z].*\([1-9]\)/ { |