diff options
Diffstat (limited to 'Doc/tools')
| -rwxr-xr-x | Doc/tools/sgmlconv/fixgenents.sh | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Doc/tools/sgmlconv/fixgenents.sh b/Doc/tools/sgmlconv/fixgenents.sh index 117b415..0503d7b 100755 --- a/Doc/tools/sgmlconv/fixgenents.sh +++ b/Doc/tools/sgmlconv/fixgenents.sh @@ -2,6 +2,9 @@ # # 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" @@ -13,7 +16,7 @@ if [ "$1" ]; then shift 1 fi -sed ' +grep -v '^<?xml .*?>$$' | sed ' s|<ABC/>|\&ABC;|g s|<ASCII/>|\&ASCII;|g s|<C/>|\&C;|g |