diff --git a/Doc/tools/sgmlconv/fixgenents.sh b/Doc/tools/sgmlconv/fixgenents.sh index 8d5f1219ef3..117b41516e2 100755 --- a/Doc/tools/sgmlconv/fixgenents.sh +++ b/Doc/tools/sgmlconv/fixgenents.sh @@ -23,6 +23,8 @@ s||\&NULL;|g s||\&POSIX;|g s||\&UNIX;|g s||\\|g +s||\≥|g s||\&hellip|g +s||\≤|g s|---|\—|g ' || exit $?