diff options
| -rwxr-xr-x | Doc/tools/sgmlconv/fixgenents.sh | 24 |
1 files changed, 0 insertions, 24 deletions
diff --git a/Doc/tools/sgmlconv/fixgenents.sh b/Doc/tools/sgmlconv/fixgenents.sh deleted file mode 100755 index 41e9e3f..0000000 --- a/Doc/tools/sgmlconv/fixgenents.sh +++ /dev/null @@ -1,24 +0,0 @@ -#! /bin/sh -# -# Script to fix general entities that got translated from the LaTeX as empty -# elements. Mostly pretty bogus, but works like a charm! -# -# Removes the leading XML PI that identifies the XML version, since most of -# the XML files are not used as top-level documents. - -if [ "$1" ]; then - exec <"$1" - shift 1 -fi - -if [ "$1" ]; then - exec >"$1" - shift 1 -fi - -sed ' -s|<geq/>|\≥|g -s|<leq/>|\≤|g -s|<geq>|\≥|g -s|<leq>|\≤|g -' || exit $? |