diff options
Diffstat (limited to 'man/example-filter.sh')
-rwxr-xr-x | man/example-filter.sh | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/man/example-filter.sh b/man/example-filter.sh new file mode 100755 index 0000000..2a71d40 --- /dev/null +++ b/man/example-filter.sh @@ -0,0 +1,22 @@ +#!/bin/sh + +# This is a super bootleg script for converting plaintext examples into groff. + +while read line; do + echo "$line" | while read -n 1 char; do + if [[ $char == "%" ]]; then + echo -n '%' + continue + fi + ord=$(printf '%d' "'$char") + if [[ $ord -eq 0 ]]; then + printf ' ' + elif [[ $ord -gt 127 ]]; then + printf '\[u%X]' "'$char" + else + printf "$char" + fi + done + echo + echo ".br" +done |