diff options
-rwxr-xr-x | util/bin/jbo | 19 |
1 files changed, 7 insertions, 12 deletions
diff --git a/util/bin/jbo b/util/bin/jbo index 78408d4f..76f86680 100755 --- a/util/bin/jbo +++ b/util/bin/jbo @@ -17,20 +17,15 @@ tr 'h' "'" | jbofihe -H | tr '\n' ' ' | sed -r ' - s@</?(HTML|HEAD|TITLE|BODY|FONT)[^>]*>@@g s@Lojban translation@@ - - s|<SUB>1</SUB>|₁|g - s|<SUB>2</SUB>|₂|g - s|<SUB>3</SUB>|₃|g - s|<SUB>4</SUB>|₄|g - s|<SUB>5</SUB>|₅|g - s|<SUB>6</SUB>|₆|g - s|<SUB>7</SUB>|₇|g - s|<SUB>8</SUB>|₈|g - s|<SUB>9</SUB>|₉|g - +' | { + sed 's:<SUB>[^>]*</SUB>:\n&\n:g' | + sed '/^<SUB>/y/0123456789/₀₁₂₃₄₅₆₇₈₉/' | + tr -d '\n' | + sed 's:</\?SUB>::g' +} | +sed -r ' s|<B>|[32m|g; s|</B>|[m|g s|<I> </I>|<I>_</I>|g |