/usr/lib/noweb/pipedocs is in noweb 2.11b-9.
This file is owned by root:root, with mode 0o755.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 | #!/bin/sh
#
# Copyright 1991 by Norman Ramsey. All rights reserved.
# See file COPYRIGHT for more information.
awk '
BEGIN {
rcsid = "$I$"
rcsname = "$Name $"
cmd = "sed '"'"'/^@begin docs /s/[0-9][0-9]*/0/'"'"' | /usr/lib/noweb/unmarkup | '"$*"' | /usr/lib/noweb/markup | grep -v '"'"'^@file $'"'"'"
}
/^@begin docs / { piping = 1 }
{ if (piping)
print | cmd
else
print
}
/^@end docs / {
piping = 0
close(cmd)
}'
|