blob: 5ac6c1d0f9845003524023a58aa335cce5cfd4b6 (
plain)
1
2
3
4
5
6
7
8
9
10
|
# whitespace -- noweb filter to make multiple whitespace
# characters equivalent to a single space, so that
# << Hello World>>, <<Hello World>>,
# and <<Hello World >> all refer to the chunk
# <<Hello World>>
sed -e '/^@use /s/[ \t][ \t]*/ /g' -e '/^@defn /s/[ \t][ \t]*/ /g' \
-e '/^@use /s/[ \t]*$//g' -e '/^@defn /s/[ \t]*$//g'
|