# whitespace -- noweb filter to make multiple whitespace # characters equivalent to a single space, so that # << Hello World>>, <>, # and <> all refer to the chunk # <> sed -e '/^@use /s/[ \t][ \t]*/ /g' -e '/^@defn /s/[ \t][ \t]*/ /g'