pdfman: convert ˆ to ^.

2017-07-17 00:16:04 +02:00 · 2017-07-17 00:16:04 +02:00 · 31aeea724e
parent 66ad2c24d4
commit 31aeea724e
1 changed files with 5 additions and 0 deletions
--- a/pdfman/pdfman
+++ b/pdfman/pdfman
@ -117,6 +117,11 @@ fi

 man -w "$@" |
    parallel 'zcat {} || cat {}' 2>/dev/null |
+    # Convert ˆ to ^
+    #   remove lines like: .    ds ^ \&
+    perl -ne '/^\s*\.\s*ds\s+\S*\^/ or print' |
+    #   replace ^ with \(ha
+    sed 's/\^/\\(ha/g' |
    # Convert -- to - and '' to "
    (echo '.tr \--'; perl -pe "s/''|\`\`/\"\"/g;") |
    man -tl - |