diff --git a/Doc/tools/sgmlconv/fixgenents.sh b/Doc/tools/sgmlconv/fixgenents.sh index 6fa36f45030..41e9e3f5d1f 100755 --- a/Doc/tools/sgmlconv/fixgenents.sh +++ b/Doc/tools/sgmlconv/fixgenents.sh @@ -17,32 +17,8 @@ if [ "$1" ]; then fi sed ' -s||ABC|g -s||ASCII|g -s||C|g -s||C++|g -s||EOF|g -s||LaTeX|g -s||NULL|g -s||POSIX|g -s||Unix|g -s||\\|g s||\≥|g -s||\&hellip|g s||\≤|g -s||\&version;|g -s||ABC|g -s||ASCII|g -s||C|g -s||C++|g -s||EOF|g -s||LaTeX|g -s||NULL|g -s||POSIX|g -s||Unix|g -s||\\|g s||\≥|g -s||\&hellip|g s||\≤|g -s||\&version;|g ' || exit $?